From 71b08b83e342f517f4255d170644cad652b680f4 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Fri, 4 Apr 2025 01:43:09 -0400
Subject: [PATCH] Finish all cases of type unique except for pair formation

---
 theories/typing_properties.v | 46 ++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

diff --git a/theories/typing_properties.v b/theories/typing_properties.v
index 67af188..b8defe3 100644
--- a/theories/typing_properties.v
+++ b/theories/typing_properties.v
@@ -46,6 +46,33 @@ Proof.
   elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
 Qed.
 
+Lemma Pair_Inv Γ a b U :
+  Γ ⊢ Pair a b ∈ U ->
+  exists A B, Γ ⊢ a ∈ A /\ Γ ⊢ b ∈ subst_Tm (scons a VarTm) B /\ Join.R (TBind TSig A B) U.
+Proof.
+  move E : (Pair a b ) => u hu.
+  move : a b E.
+  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
+Qed.
+
+Lemma ProjL_Inv Γ a U :
+  Γ ⊢ Proj PL a ∈ U ->
+  exists A B, Γ ⊢ a ∈ TBind TSig A B /\ Join.R A U.
+Proof.
+  move E : (Proj PL a) => u hu.
+  move : a E.
+  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
+Qed.
+
+Lemma ProjR_Inv Γ a U :
+  Γ ⊢ Proj PR a ∈ U ->
+  exists A B, Γ ⊢ a ∈ TBind TSig A B /\ Join.R (subst_Tm (scons (Proj PL a) VarTm) B) U.
+Proof.
+  move E : (Proj PR a) => u hu.
+  move : a E.
+  elim : Γ u U / hu => //=; hauto lq:on ctrs:Wt use:Join.reflexive, Join.transitive.
+Qed.
+
 Lemma ctx_wff_mutual :
   (forall Γ, ⊢ Γ -> True) /\
   (forall Γ a A, Γ ⊢ a ∈ A -> ⊢ Γ).
@@ -85,4 +112,23 @@ Proof.
     apply : Join.transitive; eauto.
     by apply Join.substing.
   - move => Γ a b A B i hS ihS ha iha hb ihb U.
+    move /Pair_Inv.
+    move => [A0][B0][{}/iha ha'][{}/ihb hb']hJ.
+    apply : Join.transitive; eauto.
+    apply Join.BindCong; eauto.
+    admit.
+  - move => Γ a A B ha iha U.
+    move /ProjL_Inv.
+    move => [A0][B0][{}/iha ha0]hU.
+    apply Join.BindInj in ha0.
+    decompose record ha0.
+    eauto using Join.transitive.
+  - move => Γ a A B ha iha U /ProjR_Inv [A0][B0][{}/iha /Join.BindInj ha'].
+    decompose record ha'.
+    move => h. apply : Join.transitive; eauto.
+    by apply Join.substing.
+  - move => Γ i hΓ _ B /Univ_Inv. tauto.
+  - move => Γ a A B i ha iha hb ihb.
+    move => h0 B0 {}/iha ha'.
+    eauto using Join.symmetric, Join.transitive.
 Admitted.