Work towards structural lore

DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean

@@ -389,6 +389,12 @@ theorem Subst.Eqv.liftn_append_quot {Γ : Ctx α ε} {L K : LCtx α} {J : LCtx 
   {σ : Subst.InS φ Γ L K}
   : liftn_append J ⟦σ⟧ = ⟦σ.liftn_append J⟧ := rfl
 
+theorem Subst.Eqv.vlift_liftn_append {Γ : Ctx α ε} {L K : LCtx α} {J : LCtx α}
+  {σ : Subst.Eqv φ Γ L K}
+  : (σ.liftn_append J).vlift (head := head) = σ.vlift.liftn_append J := by
+  induction σ using Quotient.inductionOn
+  simp [Subst.InS.vlift_liftn_append]
+
 @[simp]
 theorem Subst.Eqv.liftn_append_get_le {Γ : Ctx α ε} {L K : LCtx α} {J : LCtx α}
   {σ : Subst.Eqv φ Γ L K} {i : Fin (J ++ L).length}
@@ -408,6 +414,12 @@ theorem Subst.Eqv.liftn_append_singleton {Γ : Ctx α ε} {L K : LCtx α} {V : T
   : σ.liftn_append [V] = σ.slift
   := by induction σ using Quotient.inductionOn; simp
 
+@[simp]
+theorem Subst.Eqv.liftn_append_empty {Γ : Ctx α ε} {L K : LCtx α}
+  {σ : Subst.Eqv φ Γ L K}
+  : σ.liftn_append [] = σ
+  := by induction σ using Quotient.inductionOn; rw [liftn_append_quot]; congr; ext; simp
+
 @[simp]
 theorem Eqv.lsubst_cfg {Γ : Ctx α ε} {L : LCtx α}
   {R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G : ∀i, Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
@@ -432,6 +444,12 @@ theorem Subst.InS.vsubst_congr {Γ Δ : Ctx α ε} {L K : LCtx α}
   (hρ : ρ ≈ ρ') (hσ : σ ≈ σ') : σ.vsubst ρ ≈ σ'.vsubst ρ'
   := λi => Region.InS.vsubst_congr (Term.Subst.InS.slift_congr hρ) (hσ i)
 
+-- theorem Eqv.vwk_lsubst {Γ Δ : Ctx α ε}
+--   {L K : LCtx α} {σ : Subst.Eqv φ Δ L K} {ρ : Γ.InS Δ}
+--   {r : Eqv φ Δ L}
+--   : (r.lsubst σ).vwk ρ = (r.vwk ρ).lsubst (σ.vwk ρ)
+--   := sorry
+
 def Subst.Eqv.vsubst {Γ Δ : Ctx α ε} {L K : LCtx α}
   (ρ : Term.Subst.Eqv φ Γ Δ) (σ : Subst.Eqv φ Δ L K) : Subst.Eqv φ Γ L K
   := Quotient.liftOn₂ ρ σ (λρ σ => ⟦σ.vsubst ρ⟧)

DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean

@@ -198,8 +198,12 @@ theorem Eqv.packed_out_unpack {Γ : Ctx α ε} {R : LCtx α}
     simp only [Subst.Eqv.vlift_pack, vwk1_seq, nil_vwk1, vwk1_inj_l]
     rw [<-packed_out, packed_out_lwk0_arrow, I]
 
-  theorem Subst.Eqv.pack_comp_unpack {Γ : Ctx α ε} {R : LCtx α}
-    : Subst.Eqv.pack.comp Subst.Eqv.unpack = Subst.Eqv.id (φ := φ) (Γ := Γ) (L := [R.pack]) := by
+theorem Eqv.lsubst_pack_unpack {Γ : Ctx α ε} {R : LCtx α}
+  : lsubst Subst.Eqv.pack (unpack (φ := φ) (Γ := Γ) (R := R)) = nil := by
+  rw [<-Eqv.packed_out, Eqv.packed_out_unpack]
+
+theorem Subst.Eqv.pack_comp_unpack {Γ : Ctx α ε} {R : LCtx α}
+  : Subst.Eqv.pack.comp Subst.Eqv.unpack = Subst.Eqv.id (φ := φ) (Γ := Γ) (L := [R.pack]) := by
   ext ℓ
   induction ℓ using Fin.elim1
   simp only [unpack, get_comp, vlift_pack, Eqv.csubst_get, Eqv.cast_rfl, get_id, Fin.coe_fin_one]
@@ -239,6 +243,83 @@ theorem Eqv.cfg_unpack_rec {Γ : Ctx α ε} {R L : LCtx α}
 --   = cfg R β (λi => (ret (Term.Eqv.inj_n R i) ;; G).lsubst Subst.Eqv.unpack.extend)
 --   := sorry
 
+theorem Eqv.packed_out_cfg_liftn {Γ : Ctx α ε} {R L : LCtx α}
+  {β : Eqv φ Γ (R ++ L)} {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
+  : (cfg R β G).packed_out
+  = cfg R (β.lsubst (Subst.Eqv.pack.liftn_append _))
+          (λi => (G i).lsubst (Subst.Eqv.pack.liftn_append _))
+  := by simp only [packed_out, lsubst_cfg, Subst.Eqv.vlift_liftn_append, Subst.Eqv.vlift_pack]
+
+theorem Eqv.lsubst_pack_append_unpack {Γ : Ctx α ε} {L R : LCtx α}
+  : lsubst (Subst.Eqv.liftn_append R Subst.Eqv.pack).vlift (unpack (φ := φ) (Γ := Γ) (R := R ++ L))
+  = case (Term.Eqv.pack_app (e := ⊥))
+    (br (List.length R) Term.Eqv.nil (by simp))
+    (lwk_id LCtx.Wkn.id_right_append unpack) := by
+  induction R with
+  | nil => simp only [List.nil_append, Subst.Eqv.liftn_append_empty, Subst.Eqv.vlift_pack,
+    lsubst_pack_unpack, LCtx.pack.eq_1, Term.Eqv.pack_app, Term.Eqv.inj_l, List.length_nil,
+    case_inl, let1_beta, vsubst_br, Term.Eqv.nil_subst0, Term.Eqv.wk_eff_self]; rfl
+  | cons A L I =>
+    simp only [List.cons_append, LCtx.pack.eq_2, unpack, coprod, List.append_eq,
+      Eqv.nil_vwk1, lsubst_case, Term.Eqv.pack_app, Term.Eqv.coprod, List.length_cons]
+    conv => rhs; rw [case_bind, let1_case]
+    apply congrArg₂
+    · have I' := congrArg (vwk1 (inserted := ?h)) <| congrArg (lwk0 (head := A)) I
+      convert I' using 1
+      · simp [vwk1_lwk0, unpack_def, Subst.Eqv.pack]
+        congr; ext
+        simp [Region.vwk1_lwk0, Region.vwk1_lsubst]
+        simp [Region.lwk0, <-Region.lsubst_fromLwk, Region.lsubst_lsubst]
+        congr
+        funext k
+        simp only [Subst.comp, Region.lsubst, Subst.vlift, Nat.succ_eq_add_one, Function.comp_apply,
+          Subst.liftn, add_lt_add_iff_right, Region.lwk, zero_add, Nat.reduceSubDiff,
+          vsubst0_var0_vwk1, Subst.vwk1_comp_fromLwk, vwk2_vwk1, lsubst_fromLwk]
+        split <;> rfl
+      · simp [
+          lwk0, Term.Eqv.seq, let1_let1, Term.Eqv.sum, Term.Eqv.coprod, Term.Eqv.wk2, Term.Eqv.nil,
+          Nat.liftnWk, Term.Eqv.wk_lift_inj_l, <-Ctx.InS.lift_wk1, lwk_id_eq_lwk, let1_case
+        ]
+        conv => lhs; rhs; simp only [let1_beta]
+        simp [
+          Term.Eqv.inj_l, Term.Eqv.inj_r, vwk2, Nat.liftnWk, case_inl, case_inr, let1_beta, lwk_lwk,
+          vwk1_lwk]
+        congr
+        sorry
+        -- generalize Term.Eqv.pack_app (φ := φ) = P
+        -- induction P using Quotient.inductionOn
+        -- simp only [unpack_def]
+        -- apply eq_of_reg_eq
+        -- simp [<-Region.vsubst_fromWk, Region.vsubst_vsubst]
+        -- congr
+        -- funext k; cases k using Nat.cases2 <;> simp [Nat.liftnWk, Term.Subst.comp]
+        -- sorry
+    · simp only [Eqv.nil_vwk1, Term.Eqv.seq_inj_r, Term.Eqv.wk1_inr, Term.Eqv.wk1_inj_r,
+      vwk1_br, Term.Eqv.wk1_nil, vwk1_case, Term.Eqv.wk1_var0, List.length_cons, Fin.zero_eta,
+      List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, vwk2_br, Term.Eqv.wk2_nil]
+      rw [<-ret_var_zero]
+      simp only [lsubst_br, List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
+        List.getElem_cons_zero, Subst.Eqv.get_vlift, List.cons_append, lt_add_iff_pos_left,
+        add_pos_iff, zero_lt_one, or_true, Subst.Eqv.liftn_append_get_le, vwk1_br,
+        Term.Eqv.wk1_var0, vwk_id_eq, vsubst_br, Term.Eqv.var0_subst0, Term.Eqv.wk_res_self,
+        Term.Eqv.inj_r, vwk2, lwk_id_eq_lwk, Set.mem_setOf_eq, lwk_case, lwk_quot, vwk1_case,
+        LCtx.pack.eq_2, vwk_quot, vwk_case, Term.Eqv.wk_var, Ctx.InS.coe_wk2, Nat.liftnWk,
+        Nat.ofNat_pos, ↓reduceIte, let1_beta, vsubst_case, Term.Eqv.subst_lift_nil,
+        Term.Eqv.subst_lift_var_zero, case_inr, Nat.add_zero, Nat.zero_eq, ↓dreduceIte,
+        Nat.reduceSub, Nat.succ_eq_add_one, Nat.reduceAdd]
+      apply eq_of_reg_eq
+      simp
+
+
+theorem Eqv.unpacked_out_pack_liftn {Γ : Ctx α ε} {R L : LCtx α}
+  {β : Eqv φ Γ [(R ++ L).pack]}
+  : β.unpacked_out.lsubst (Subst.Eqv.pack.liftn_append R)
+  = β.lsubst (case (Term.Eqv.pack_app (e := ⊥))
+    (br R.length Term.Eqv.nil (by simp))
+    (unpack.lwk_id LCtx.Wkn.id_right_append)).csubst := by
+  rw [unpacked_out, lsubst_lsubst]; congr; ext k; cases k using Fin.elim1
+  simp [Subst.Eqv.get_comp, Subst.Eqv.unpack_zero, lsubst_pack_append_unpack]
+
 end Region
 
 end BinSyntax

DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Sum.lean

@@ -289,6 +289,11 @@ theorem Eqv.coprod_seq {A B C : Ty α} {Γ : Ctx α ε}
   : coprod l r ;;' f = coprod (l ;;' f) (r ;;' f)
   := by rw [coprod, seq, let1_case, coprod, wk1_seq, wk1_seq]; rfl
 
+theorem Eqv.wk_lift_coprod {A B C : Ty α} {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ}
+  {l : Eqv φ ((A, ⊥)::Δ) ⟨C, e⟩} {r : Eqv φ ((B, ⊥)::Δ) ⟨C, e⟩}
+  : wk ρ.slift (coprod l r) = coprod (wk ρ.slift l) (wk ρ.slift r)
+  := by simp [coprod, wk1, wk_wk]; congr 2 <;> ext k <;> cases k <;> rfl
+
 def Eqv.inj_l {A B : Ty α} {Γ : Ctx α ε} : Eqv (φ := φ) (⟨A, ⊥⟩::Γ) ⟨A.coprod B, e⟩
   := inl nil
 
@@ -297,6 +302,11 @@ theorem Eqv.wk1_inj_l {A B : Ty α} {Γ : Ctx α ε}
   : (inj_l (φ := φ) (e := e) (A := A) (B := B) (Γ := Γ)).wk1 (inserted := inserted) = inj_l
   := by simp [inj_l]
 
+@[simp]
+theorem Eqv.wk_lift_inj_l {A B : Ty α} {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ}
+  : wk ρ.slift (inj_l (φ := φ) (e := e) (A := A) (B := B)) = inj_l
+  := by simp [inj_l]
+
 @[simp]
 theorem Eqv.wk2_inj_l {A B : Ty α} {Γ : Ctx α ε}
   : (inj_l (φ := φ) (e := e) (A := A) (B := B) (Γ := head::Γ)).wk2 (inserted := inserted) = inj_l
@@ -320,6 +330,11 @@ theorem Eqv.wk1_inj_r {A B : Ty α} {Γ : Ctx α ε}
   : (inj_r (φ := φ) (e := e) (A := A) (B := B) (Γ := Γ)).wk1 (inserted := inserted) = inj_r
   := by simp [inj_r]
 
+@[simp]
+theorem Eqv.wk_lift_inj_r {A B : Ty α} {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ}
+  : wk ρ.slift (inj_r (φ := φ) (e := e) (A := A) (B := B)) = inj_r
+  := by simp [inj_r]
+
 @[simp]
 theorem Eqv.wk2_inj_r {A B : Ty α} {Γ : Ctx α ε}
   : (inj_r (φ := φ) (e := e) (A := A) (B := B) (Γ := head::Γ)).wk2 (inserted := inserted) = inj_r

DeBruijnSSA/BinSyntax/Rewrite/Term/Structural/Sum.lean

@@ -9,26 +9,37 @@ variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [O
 namespace Term
 
 set_option linter.unusedVariables false in
-def Eqv.inj
+def Eqv.inj'
   {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} (a : Eqv φ Γ (R.get i, e)) : Eqv φ Γ (R.pack, e)
   := match R with
   | [] => i.elim0
-  | _::R => by cases i using Fin.cases with | zero => exact a.inr | succ i => exact inl (inj a)
+  | _::R => by cases i using Fin.cases with | zero => exact a.inr | succ i => exact inl (inj' a)
 
 @[simp]
-theorem Eqv.inj_quot {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {a : InS φ Γ (R.get i, e)}
-  : Eqv.inj ⟦a⟧ = ⟦Term.InS.inj a⟧ := by
+theorem Eqv.inj_quot' {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {a : InS φ Γ (R.get i, e)}
+  : Eqv.inj' ⟦a⟧ = ⟦Term.InS.inj a⟧ := by
   induction R generalizing Γ with
   | nil => exact i.elim0
   | cons _ _ I =>
     cases i using Fin.cases with
     | zero => rfl
     | succ i =>
-      simp only [inj, I, inl_quot, Fin.cases_succ]
+      simp only [inj', I, inl_quot, Fin.cases_succ]
       apply congrArg
       ext
       simp [Term.inj, Term.Wf.inj, -Function.iterate_succ, Function.iterate_succ']
 
+def Eqv.inj
+  {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} (a : Eqv φ Γ (R.get i, e)) : Eqv φ Γ (R.pack, e)
+  := Quotient.liftOn a (λa => ⟦a.inj⟧) (λ_ _ h => by simp [<-Eqv.inj_quot', Quotient.sound h])
+
+@[simp]
+theorem Eqv.inj_quot {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {a : InS φ Γ (R.get i, e)}
+  : Eqv.inj ⟦a⟧ = ⟦a.inj⟧ := rfl
+
+theorem Eqv.inj_eq_inj' {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {a : Eqv φ Γ (R.get i, e)}
+  : a.inj = Eqv.inj' a := by induction a using Quotient.inductionOn; rw [inj_quot']; rfl
+
 @[simp]
 theorem Eqv.wk_inj {Γ Δ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
   {a : Eqv φ Δ (R.get i, e)} {ρ : Γ.InS Δ}
@@ -61,7 +72,7 @@ theorem Eqv.inj_zero {Γ : Ctx α ε} {R : LCtx α}
 
 theorem Eqv.inj_succ {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
   {a : Eqv φ Γ (List.get (A::R) i.succ, e)}
-  : a.inj = (a.inj (R := R)).inl := rfl
+  : a.inj = (a.inj (R := R)).inl := by rw [inj_eq_inj', inj_eq_inj']; rfl
 
 def Eqv.inj_n {Γ : Ctx α ε} (R : LCtx α) (i : Fin R.length) : Eqv φ ((R.get i, ⊥)::Γ) (R.pack, e)
   := match R with
@@ -97,24 +108,67 @@ theorem Eqv.seq_inj_n  {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
   | cons _ _ I =>
     cases i using Fin.cases with
     | zero => simp [inj_n, <-inr_let1, nil, let1_eta]
-    | succ i => simp [inj_n, <-inl_let1, I, inj]
+    | succ i => simp [inj_n, <-inl_let1, I, inj_succ]
 
--- def Eqv.pack_case {Γ : Ctx α ε} {R : LCtx α}
---   (d : Eqv φ Γ (R.pack, e)) (G : ∀i : Fin R.length, Eqv φ ((R.get i, ⊥)::Γ) (A, e))
---   : Eqv φ Γ (C, e) := sorry
+def Eqv.pack_app_inr {Γ : Ctx α ε} {L R : LCtx α} : Eqv φ ((L.pack, ⊥)::Γ) ((L ++ R).pack, e)
+  := match L with
+  | [] => zero
+  | _::_ => coprod (pack_app_inr ;;' inj_l) inj_r
 
--- def Eqv.pack_app_inl {Γ : Ctx α ε} {L R : LCtx α} : Eqv φ ((L.pack, ⊥)::Γ) ((L ++ R).pack, e)
---   := sorry
+def Eqv.pack_app_inl {Γ : Ctx α ε} {L R : LCtx α} : Eqv φ ((R.pack, ⊥)::Γ) ((L ++ R).pack, e)
+  := match L with
+  | [] => nil
+  | _::_ => pack_app_inl ;;' inj_l
 
--- def Eqv.pack_app_inr {Γ : Ctx α ε} {L R : LCtx α} : Eqv φ ((R.pack, ⊥)::Γ) ((L ++ R).pack, e)
---   := sorry
+def Eqv.pack_app {Γ : Ctx α ε} {L R : LCtx α}
+  : Eqv φ (((L ++ R).pack, ⊥)::Γ) (R.pack.coprod L.pack, e)
+  := match L with
+  | [] => inj_l
+  | _::L => coprod (pack_app (L := L) ;;' sum nil inj_l) (inj_r ;;' inj_r)
 
--- def Eqv.pack_app {Γ : Ctx α ε} {L R : LCtx α}
---   : Eqv φ (((L ++ R).pack, ⊥)::Γ) (L.pack.coprod R.pack, e)
---   := sorry
-
--- TODO: pack_app
+@[simp]
+theorem Eqv.wk_lift_pack_app {Γ Δ : Ctx α ε} {L R : LCtx α} {ρ : Γ.InS Δ}
+  : (pack_app (φ := φ) (Γ := Δ) (L := L) (R := R) (e := e)).wk ρ.slift = pack_app := by
+  induction L generalizing R with
+  | nil => rfl
+  | cons A L I => simp [pack_app, wk_lift_seq, Term.Eqv.wk_lift_coprod, Term.Eqv.sum, I]
 
--- TODO: pack_app_pack_case => pack_case
+@[simp]
+theorem Eqv.wk1_pack_app {Γ : Ctx α ε} {L R : LCtx α}
+  : (pack_app (φ := φ) (Γ := Γ) (L := L) (R := R) (e := e)).wk1 (inserted := inserted) = pack_app
+  := by rw [wk1, <-Ctx.InS.lift_wk0, wk_lift_pack_app]
+
+theorem Eqv.pack_app_coprod {Γ : Ctx α ε} {L R : LCtx α}
+  : pack_app (φ := φ) (Γ := Γ) (L := L) (R := R) (e := e) ;;' coprod pack_app_inl pack_app_inr = nil
+  := by induction L generalizing R with
+  | nil => simp [pack_app, pack_app_inl, inj_l_coprod]
+  | cons A L I =>
+    simp only [List.cons_append, LCtx.pack.eq_2, pack_app, List.append_eq, coprod_seq, ← seq_assoc,
+      sum_coprod, nil_seq, inj_r_coprod]
+    simp [
+      pack_app_inl, pack_app_inr, inj_l_coprod, inj_r_coprod, <-coprod_seq, seq_assoc, I,
+      coprod_inl_inr
+    ]
+
+theorem Eqv.pack_app_inl_pack_app {Γ : Ctx α ε} {L R : LCtx α}
+  : pack_app_inl ;;' pack_app (φ := φ) (Γ := Γ) (L := L) (R := R) (e := e) = inj_l
+  := by induction L generalizing R with
+  | nil => simp [pack_app_inl, pack_app, inj_l_coprod]
+  | cons A L I =>
+    simp only [LCtx.pack.eq_2, List.cons_append, pack_app_inl, pack_app, List.append_eq, ←
+      seq_assoc, inj_l_coprod]
+    rw [seq_assoc, I, sum, inj_l_coprod, nil_seq]
+
+theorem Eqv.pack_app_inr_pack_app {Γ : Ctx α ε} {L R : LCtx α}
+  : pack_app_inr ;;' pack_app (φ := φ) (Γ := Γ) (L := L) (R := R) (e := e) = inj_r
+  := by induction L generalizing R with
+  | nil => apply zero_eq
+  | cons A L I =>
+    simp [pack_app_inr, pack_app, coprod_seq, <-seq_assoc, inj_l_coprod, inj_r_coprod]
+    rw [seq_assoc, I, sum, inj_r_coprod, <-coprod_seq, coprod_inl_inr, nil_seq]
+
+theorem Eqv.coprod_pack_app {Γ : Ctx α ε} {L R : LCtx α}
+  : coprod pack_app_inl pack_app_inr ;;' pack_app (φ := φ) (Γ := Γ) (L := L) (R := R) (e := e) = nil
+  := by simp [coprod_seq, pack_app_inl_pack_app, pack_app_inr_pack_app, coprod_inl_inr]
 
 end Term

DeBruijnSSA/BinSyntax/Typing/LCtx.lean

@@ -354,16 +354,42 @@ theorem LCtx.IsInitial.pack {L : LCtx α} : L.IsInitial → Ty.IsInitial (LCtx.p
   := pack_iff.mpr
 
 @[simp]
-def LCtx.pack' : LCtx α → Ty α
-  | [] => Ty.empty
-  | [A] => A
-  | A::L => Ty.coprod A (pack' L)
+def LCtx.dist (X : Ty α) : LCtx α → LCtx α
+  | [] => []
+  | A::L => (Ty.prod X A)::(dist X L)
 
-theorem LCtx.IsInitial.pack_iff' {L : LCtx α} : L.pack'.IsInitial ↔ L.IsInitial := by
-  induction L with | nil => simp | cons _ L I => cases L <;> simp [*]
+theorem LCtx.IsInitial.dist_iff {X : Ty α} {L : LCtx α}
+  : (L.dist X).IsInitial ↔ X.IsInitial ∨ L.IsInitial
+  := by induction L <;> aesop
 
-theorem LCtx.IsInitial.pack' {L : LCtx α} : L.IsInitial → Ty.IsInitial (LCtx.pack L)
-  := pack_iff.mpr
+theorem LCtx.IsInitial.dist {X : Ty α} {L : LCtx α}
+  : L.IsInitial → (L.dist X).IsInitial
+  := dist_iff.mpr ∘ Or.inr
+
+theorem Ty.IsInitial.dist {X : Ty α} {L : LCtx α}
+  : X.IsInitial → (L.dist X).IsInitial
+  := LCtx.IsInitial.dist_iff.mpr ∘ Or.inl
+
+theorem LCtx.length_dist {X : Ty α} {L : LCtx α} : (L.dist X).length = L.length
+  := by induction L <;> simp [*]
+
+theorem LCtx.getElem_dist {X : Ty α} {L : LCtx α} {n} {h : n < (L.dist X).length}
+  : (L.dist X)[n] = Ty.prod X (L[n]'(L.length_dist ▸ h))
+  := by induction L generalizing n with
+  | nil => cases h
+  | cons _ _ I => cases n <;> simp [*]
+
+theorem LCtx.get_dist {X : Ty α} {L : LCtx α} {i}
+  : (L.dist X).get i = Ty.prod X (L.get <| i.cast L.length_dist)
+  := getElem_dist
+
+@[simp]
+def LCtx.dpack (X : Ty α) : LCtx α → Ty α
+  | [] => Ty.empty
+  | A::L => Ty.coprod (dpack X L) (Ty.prod X A)
+
+theorem LCtx.pack_dist {X : Ty α} {L : LCtx α} : LCtx.pack (L.dist X) = LCtx.dpack X L := by
+  induction L <;> simp [*]
 
 def Ty.unpack_sum : Ty α → LCtx α
   | Ty.empty => []

DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean

@@ -633,6 +633,11 @@ theorem Region.Subst.InS.vlift_slift {Γ : Ctx α ε} {L K : LCtx α}
   {σ : Subst.InS φ Γ L K}
   : (σ.slift (head := head')).vlift (head := head) = σ.vlift.slift := vlift_lift
 
+theorem Region.Subst.InS.vlift_liftn_append {Γ : Ctx α ε} {L K J : LCtx α}
+  {σ : Subst.InS φ Γ L K}
+  : (σ.liftn_append J).vlift (head := head) = σ.vlift.liftn_append J := by
+  ext; simp [Region.Subst.vlift_liftn_comm]
+
 theorem Region.InS.vwk1_lsubst_vlift {Γ : Ctx α ε} {L K : LCtx α}
   {σ : Subst.InS φ Γ L K} {r : Region.InS φ (head::Γ) L}
   : (r.lsubst σ.vlift).vwk1 (inserted := inserted) = r.vwk1.lsubst σ.vlift.vlift := by