Work on associator lore

DeBruijnSSA/BinSyntax/Rewrite/Term/Compose.lean

@@ -25,11 +25,20 @@ theorem Eqv.wk2_nil {A : Ty α} {Γ : Ctx α ε}
   : (nil (φ := φ) (A := A) (Γ := head::Γ) (e := e)).wk2 (inserted := inserted) = nil
   := rfl
 
+@[simp]
+theorem Eqv.subst_lift_nil {A : Ty α} {Γ : Ctx α ε} {σ : Subst.Eqv φ Γ Δ} {h}
+  : (nil : Eqv φ (⟨A, ⊥⟩::Δ) ⟨A, e⟩).subst (σ.lift h) = nil := by
+  induction σ using Quotient.inductionOn; rfl
+
 @[simp]
 theorem Eqv.wk_eff_nil {A : Ty α} {Γ : Ctx α ε} (h : lo ≤ hi)
   : (nil (φ := φ) (A := A) (Γ := Γ)).wk_eff h = nil
   := rfl
 
+theorem Eqv.nil_pure {A : Ty α} {Γ : Ctx α ε}
+  : (nil : Eqv φ (⟨A, ⊥⟩::Γ) ⟨A, e⟩) = nil.wk_eff bot_le
+  := rfl
+
 @[simp]
 theorem Eqv.subst0_nil_wk1 {Γ : Ctx α ε}
   (a : Eqv φ (⟨A, ⊥⟩::Γ) V) : a.wk1.subst nil.subst0 = a
@@ -41,8 +50,8 @@ theorem Eqv.nil_subst0 {Γ : Ctx α ε} (a : Eqv φ Γ ⟨A, ⊥⟩)
   := by induction a using Quotient.inductionOn; rfl
 
 @[simp]
-theorem Eqv.nil_pure {A : Ty α} {Γ : Ctx α ε} : (nil (φ := φ) (A := A) (Γ := Γ) (e := e)).Pure
-  := ⟨nil, rfl⟩
+theorem Eqv.Pure.nil {A : Ty α} {Γ : Ctx α ε} : (nil (φ := φ) (A := A) (Γ := Γ) (e := e)).Pure
+  := ⟨Eqv.nil, rfl⟩
 
 def Eqv.seq {A B C : Ty α} {Γ : Ctx α ε}
 (a : Eqv φ ((A, ⊥)::Γ) (B, e)) (b : Eqv φ ((B, ⊥)::Γ) (C, e))
@@ -422,6 +431,12 @@ theorem Eqv.swap_ltimes {A B B' : Ty α} {Γ : Ctx α ε}
   (l : Eqv φ (⟨B, ⊥⟩::Γ) ⟨B', e⟩) : swap ;;' ltimes l A = rtimes A l ;;' swap := by
   rw [<-seq_swap_inj, swap_ltimes_swap, <-seq_assoc, swap_swap, seq_nil]
 
+theorem Eqv.rtimes_swap {A B B' : Ty α} {Γ : Ctx α ε}
+  (r : Eqv φ (⟨B, ⊥⟩::Γ) ⟨B', e⟩) : rtimes A r ;;' swap = swap ;;' ltimes r A := by rw [swap_ltimes]
+
+theorem Eqv.ltimes_swap {A B B' : Ty α} {Γ : Ctx α ε}
+  (l : Eqv φ (⟨B, ⊥⟩::Γ) ⟨B', e⟩) : ltimes l A ;;' swap = swap ;;' rtimes A l := by rw [swap_rtimes]
+
 theorem Eqv.rtimes_nil {A B : Ty α} {Γ : Ctx α ε}
   : rtimes (φ := φ) (Γ := Γ) (A := A) (B := B) (B' := B) (e := e) nil = nil := tensor_nil_nil
 
@@ -454,13 +469,36 @@ theorem Eqv.ltimes_rtimes {A A' B B' : Ty α} {Γ : Ctx α ε}
 theorem Eqv.Pure.left_central {A A' B B' : Ty α} {Γ : Ctx α ε}
   {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨A', e⟩} (hl : l.Pure) (r : Eqv φ (⟨B, ⊥⟩::Γ) ⟨B', e⟩)
   : ltimes l B ;;' rtimes A' r = rtimes A r ;;' ltimes l B':= by
-  rw [<-swap_rtimes_swap (r := l) (A := B'), seq_assoc]
-  sorry
+  rw [ltimes_rtimes, seq_ltimes, tensor, rtimes, tensor, let2_let2]
+  apply congrArg
+  rw [let2_pair]
+  simp only [wk1_nil, wk0_nil, wk2_pair, wk2_nil, let1_beta_var1, subst_let1, subst0_wk0,
+    subst_pair, subst_lift_nil]
+  apply Eq.symm
+  rw [pair_bind_left]
+  apply Eq.symm
+  rw [pair_bind_swap_left]
+  -- TODO: this REALLY needs to be factored out...
+  congr
+  induction l using Quotient.inductionOn
+  apply eq_of_term_eq
+  simp only [Set.mem_setOf_eq, InS.coe_wk, Ctx.InS.coe_wk0, Ctx.InS.coe_wk1, ← subst_fromWk,
+    Term.subst_subst, InS.coe_subst, Subst.coe_lift, InS.coe_subst0, InS.coe_var, Ctx.InS.coe_wk2]
+  congr
+  funext k
+  cases k <;> rfl
+  sorry -- TODO: obviously, if something is pure so are its weakenings
 
 theorem Eqv.Pure.right_central {A A' B B' : Ty α} {Γ : Ctx α ε}
   (l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨A', e⟩) {r : Eqv φ (⟨B, ⊥⟩::Γ) ⟨B', e⟩} (hr : r.Pure)
   : ltimes l B ;;' rtimes A' r = rtimes A r ;;' ltimes l B'
-  := by sorry
+  := by
+  apply Eq.symm
+  rw [
+    <-swap_ltimes_swap, <-seq_assoc, swap_ltimes (l := l), seq_assoc, <-seq_assoc (a := swap),
+    hr.left_central, seq_assoc, swap_rtimes, <-seq_assoc, ltimes_swap (l := r), seq_assoc,
+    <-seq_assoc (c := swap), swap_swap, seq_nil
+  ]
 
 theorem Eqv.tensor_seq_of_comm {A₀ A₁ A₂ B₀ B₁ B₂ : Ty α} {Γ : Ctx α ε}
   {l : Eqv φ (⟨A₀, ⊥⟩::Γ) ⟨A₁, e⟩} {r : Eqv φ (⟨B₀, ⊥⟩::Γ) ⟨B₁, e⟩}
@@ -473,8 +511,6 @@ theorem Eqv.tensor_seq_of_comm {A₀ A₁ A₂ B₀ B₁ B₂ : Ty α} {Γ : Ctx
 
 -- TODO: tensor_seq (pure only)
 
--- TODO: swap
-
 def Eqv.split {A : Ty α} {Γ : Ctx α ε} : Eqv (φ := φ) (⟨A, ⊥⟩::Γ) ⟨A.prod A, e⟩
   := let1 nil (pair nil nil)
 
@@ -492,7 +528,55 @@ def Eqv.assoc_inv {A B C : Ty α} {Γ : Ctx α ε}
   let2 (var (V := (B.prod C, e)) 0 (by simp)) $
   pair (pair (var 3 (by simp)) (var 1 (by simp))) (var 0 (by simp))
 
--- TODO: assoc_assoc_inv, assoc_inv_assoc
+theorem Eqv.seq_prod_assoc {A B C : Ty α} {Γ : Ctx α ε}
+  (r : Eqv φ (⟨X, ⊥⟩::Γ) ⟨(A.prod B).prod C, e⟩)
+  : r ;;' assoc = (let2 r $ let2 (var (V := (A.prod B, e)) 1 (by simp))
+                          $ pair (var 1 (by simp)) (pair (var 0 (by simp)) (var 2 (by simp))))
+   := sorry
+
+theorem Eqv.seq_assoc_inv {A B C : Ty α} {Γ : Ctx α ε}
+  (r : Eqv φ (⟨X, ⊥⟩::Γ) ⟨A.prod (B.prod C), e⟩)
+  : r ;;' assoc_inv = (let2 r $ let2 (var (V := (B.prod C, e)) 0 (by simp))
+                              $ pair (pair (var 3 (by simp)) (var 1 (by simp))) (var 0 (by simp)))
+  := sorry
+
+@[simp]
+theorem Eqv.wk_eff_assoc {A B C : Ty α} {Γ : Ctx α ε} {h : lo ≤ hi}
+  : (assoc (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := lo)).wk_eff h = assoc := rfl
+
+@[simp]
+theorem Eqv.wk_eff_assoc_inv {A B C : Ty α} {Γ : Ctx α ε} {h : lo ≤ hi}
+  : (assoc_inv (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := lo)).wk_eff h = assoc_inv := rfl
+
+theorem Eqv.assoc_pure  {A B C : Ty α} {Γ : Ctx α ε}
+  : assoc (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e) = assoc.wk_eff bot_le
+  := rfl
+
+theorem Eqv.assoc_inv_pure {A B C : Ty α} {Γ : Ctx α ε}
+  : assoc_inv (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e) = assoc_inv.wk_eff bot_le
+  := rfl
+
+@[simp]
+theorem Eqv.Pure.assoc {A B C : Ty α} {Γ : Ctx α ε}
+  : (assoc (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e)).Pure := ⟨Eqv.assoc, rfl⟩
+
+@[simp]
+theorem Eqv.Pure.assoc_inv {A B C : Ty α} {Γ : Ctx α ε}
+  : (assoc_inv (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e)).Pure := ⟨Eqv.assoc_inv, rfl⟩
+
+theorem Eqv.assoc_assoc_inv_pure {A B C : Ty α} {Γ : Ctx α ε}
+  : assoc (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := ⊥) ;;' assoc_inv = nil := sorry
+
+theorem Eqv.assoc_inv_assoc_pure {A B C : Ty α} {Γ : Ctx α ε}
+  : assoc_inv (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := ⊥) ;;' assoc = nil := sorry
+
+theorem Eqv.assoc_assoc_inv {A B C : Ty α} {Γ : Ctx α ε}
+  : assoc (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e) ;;' assoc_inv = nil :=  by
+  rw [assoc_pure, assoc_inv_pure, <-wk_eff_seq, assoc_assoc_inv_pure]; rfl
+
+theorem Eqv.assoc_inv_assoc {A B C : Ty α} {Γ : Ctx α ε}
+  : assoc_inv (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e) ;;' assoc = nil := by
+  rw [assoc_pure, assoc_inv_pure, <-wk_eff_seq, assoc_inv_assoc_pure]; rfl
 
 def Eqv.coprod {A B C : Ty α} {Γ : Ctx α ε}
   (l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨C, e⟩) (r : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, e⟩)

DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean

@@ -24,6 +24,9 @@ theorem Eqv.sound {a a' : InS φ Γ V} (h : a ≈ a') : InS.q a = InS.q a' := Qu
 
 theorem Eqv.eq {a a' : InS φ Γ V} : a.q = a'.q ↔ a ≈ a' := Quotient.eq
 
+theorem Eqv.eq_of_term_eq {a a' : InS φ Γ V} (h : (a : Term φ) = (a' : Term φ))
+  : a.q = a'.q := sorry
+
 def Eqv.var (n : ℕ) (hn : Γ.Var n V) : Eqv φ Γ V := ⟦InS.var n hn⟧
 
 def Eqv.op (f : φ) (hf : Φ.EFn f A B e) (a : Eqv φ Γ ⟨A, e⟩) : Eqv φ Γ ⟨B, e⟩
@@ -474,6 +477,8 @@ theorem Eqv.subst_var_wk0 {σ : Subst.Eqv φ Γ Δ} {n : ℕ}
   induction σ using Quotient.inductionOn
   rfl
 
+def Subst.Eqv.fromWk (ρ : Γ.InS Δ) : Eqv φ Γ Δ := ⟦Subst.InS.fromWk ρ⟧
+
 -- TODO: subst_var lore
 
 @[simp]
@@ -897,6 +902,119 @@ theorem Eqv.initial (hΓ : Γ.IsInitial) {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ
   induction a using Quotient.inductionOn; induction b using Quotient.inductionOn; apply sound;
   apply InS.initial hΓ
 
+-- TODO: eqv induction...
+
+theorem Eqv.let1_wk_eff_let1 {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A, ⊥⟩} {b : Eqv φ Γ ⟨B, e⟩} {c : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨C, e⟩}
+  : let1 (a.wk_eff bot_le) (let1 b.wk0 c)
+  = let1 b (let1 (a.wk_eff bot_le).wk0 (c.wk Ctx.InS.swap01)) := by
+  rw [let1_beta, wk0_wk_eff, let1_beta, subst_let1, subst0_wk0]
+  apply congrArg
+  induction c using Quotient.inductionOn
+  induction a using Quotient.inductionOn
+  apply Eqv.eq_of_term_eq
+  simp only [Set.mem_setOf_eq, InS.coe_subst, Subst.coe_lift, InS.coe_subst0, InS.coe_wk0,
+    InS.coe_wk, Ctx.InS.coe_swap01, ← subst_fromWk, Term.subst_subst]
+  congr
+  funext k
+  cases k with
+  | zero => rfl
+  | succ k => cases k with
+  | zero => simp [Term.Subst.comp, Term.subst_fromWk]
+  | succ k => rfl
+
+theorem Eqv.Pure.let1_let1 {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B, e⟩} {c : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨C, e⟩}
+  : a.Pure → let1 a (let1 b.wk0 c) = let1 b (let1 a.wk0 (c.wk Ctx.InS.swap01))
+  | ⟨a, ha⟩ => by cases ha; rw [let1_wk_eff_let1]
+
+theorem Eqv.let1_let1_comm {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A, ⊥⟩} {b : Eqv φ Γ ⟨B, ⊥⟩} {c : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨C, ⊥⟩}
+  : let1 a (let1 b.wk0 c) = let1 b (let1 a.wk0 (c.wk Ctx.InS.swap01))
+  := Eqv.Pure.let1_let1 ⟨a, by simp⟩
+
+theorem Eqv.swap01_let2_eta {Γ : Ctx α ε} {A B : Ty α} {e}
+  : (pair (var 1 (by simp)) (var 0 (by simp)) : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) (A.prod B, e)
+    ).wk Ctx.InS.swap01 = pair (var 0 (by simp)) (var 1 (by simp)) := rfl
+
+theorem Eqv.pair_bind_swap_left
+  {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B, e⟩}
+  (ha : a.Pure)
+  : pair a b = (let1 b $ let1 a.wk0 $ pair (var 0 (by simp)) (var 1 (by simp))) := by
+  rw [pair_bind, ha.let1_let1, swap01_let2_eta]
+
+theorem Eqv.pair_bind_swap_right
+  {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B, e⟩}
+  (hb : b.Pure)
+  : pair a b = (let1 b $ let1 a.wk0 $ pair (var 0 (by simp)) (var 1 (by simp))) := by
+  rw [pair_bind, hb.let1_let1]; rfl
+
+theorem Eqv.pair_bind_swap_wk_eff_left {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A, ⊥⟩} {b : Eqv φ Γ ⟨B, e⟩}
+  : pair (a.wk_eff bot_le) b
+  = (let1 b $ let1 (a.wk_eff bot_le).wk0 $ pair (var 0 (by simp)) (var 1 (by simp)))
+  := pair_bind_swap_left ⟨a, rfl⟩
+
+theorem Eqv.pair_bind_swap_wk_eff_right {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B, ⊥⟩}
+  : pair a (b.wk_eff bot_le)
+  = (let1 (b.wk_eff bot_le) $ let1 a.wk0 $ pair (var 0 (by simp)) (var 1 (by simp)))
+  := pair_bind_swap_right ⟨b, rfl⟩
+
+theorem Eqv.pair_bind_swap
+  {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, ⊥⟩} {b : Eqv φ Γ ⟨B, ⊥⟩}
+  : pair a b = (let1 b $ let1 a.wk0 $ pair (var 0 (by simp)) (var 1 (by simp)))
+  := pair_bind_swap_left ⟨a, by simp⟩
+
+def Eqv.reassoc {A B C : Ty α} {Γ : Ctx α ε}
+  (r : Eqv φ Γ ⟨(A.prod B).prod C, e⟩)
+  : Eqv φ Γ ⟨A.prod (B.prod C), e⟩
+  := let2 r
+  $ let2 (var (V := (A.prod B, e)) 1 (by simp))
+  $ pair (var 1 (by simp)) (pair (var 0 (by simp)) (var 2 (by simp)))
+
+def Eqv.reassoc_inv {A B C : Ty α} {Γ : Ctx α ε}
+  (r : Eqv φ Γ ⟨A.prod (B.prod C), e⟩)
+  : Eqv φ Γ ⟨(A.prod B).prod C, e⟩
+  := let2 r
+  $ let2 (var (V := (B.prod C, e)) 0 (by simp))
+  $ pair (pair (var 3 (by simp)) (var 1 (by simp))) (var 0 (by simp))
+
+theorem Eqv.reassoc_beta {A B C : Ty α} {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B, e⟩} {c : Eqv φ Γ ⟨C, e⟩}
+  : reassoc (pair (pair a b) c) = pair a (pair b c) := by sorry
+
+theorem Eqv.reassoc_inv_beta {A B C : Ty α} {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B, e⟩} {c : Eqv φ Γ ⟨C, e⟩}
+  : reassoc_inv (pair a (pair b c)) = pair (pair a b) c := by sorry
+
+theorem Eqv.let1_reassoc {A B C : Ty α} {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨X, e⟩}
+  {r : Eqv φ ((X, ⊥)::Γ) ⟨(A.prod B).prod C, e⟩}
+  : let1 a (reassoc r) = reassoc (let1 a r) := sorry
+
+theorem Eqv.let2_reassoc {A B C : Ty α} {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨X.prod Y, e⟩}
+  {r : Eqv φ ((Y, ⊥)::(X, ⊥)::Γ) ⟨(A.prod B).prod C, e⟩}
+  : let2 a (reassoc r) = reassoc (let2 a r) := sorry
+
+theorem Eqv.case_reassoc {A B C : Ty α} {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨Ty.coprod X Y, e⟩}
+  {l : Eqv φ (⟨X, ⊥⟩::Γ) ⟨(A.prod B).prod C, e⟩}
+  {r : Eqv φ (⟨Y, ⊥⟩::Γ) ⟨(A.prod B).prod C, e⟩}
+  : case a (reassoc l) (reassoc r) = reassoc (case a l r) := by
+  sorry
+
+theorem Eqv.let1_reassoc_inv {A B C : Ty α} {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨X, e⟩}
+  {r : Eqv φ ((X, ⊥)::Γ) ⟨A.prod (B.prod C), e⟩}
+  : let1 a (reassoc_inv r) = reassoc_inv (let1 a r) := sorry
+
+theorem Eqv.let2_reassoc_inv {A B C : Ty α} {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨X.prod Y, e⟩}
+  {r : Eqv φ ((Y, ⊥)::(X, ⊥)::Γ) ⟨A.prod (B.prod C), e⟩}
+  : let2 a (reassoc_inv r) = reassoc_inv (let2 a r) := sorry
+
 end Basic
 
 end Term

DeBruijnSSA/BinSyntax/Rewrite/Term/Induction.lean

@@ -0,0 +1,12 @@
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Setoid
+
+import Discretion.Utils.Quotient
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Term
+
+
+-- ...

DeBruijnSSA/BinSyntax/Typing/Ctx.lean

@@ -269,13 +269,31 @@ theorem Wkn.swap01 {left right : Ty α × ε} {Γ : Ctx α ε}
   | 1, _ => by simp
   | n + 2, hn => ⟨hn, by simp⟩
 
+def InS.swap01 {left right : Ty α × ε} {Γ : Ctx α ε}
+  : InS (left::right::Γ) (right::left::Γ)
+  := ⟨Nat.swap0 1, Wkn.swap01⟩
+
+@[simp]
+theorem InS.coe_swap01 {left right : Ty α × ε} {Γ : Ctx α ε}
+  : (InS.swap01 (Γ := Γ) (left := left) (right := right) : ℕ → ℕ) = Nat.swap0 1
+  := rfl
+
 theorem Wkn.swap02 {first second third : Ty α × ε} {Γ : Ctx α ε}
   : Wkn (first::second::third::Γ) (third::first::second::Γ) (Nat.swap0 2)
   | 0, _ => by simp
   | 1, _ => by simp
   | 2, _ => by simp
   | n + 3, hn => ⟨hn, by simp⟩
 
+def InS.swap02 {first second third : Ty α × ε} {Γ : Ctx α ε}
+  : InS (first::second::third::Γ) (third::first::second::Γ)
+  := ⟨Nat.swap0 2, Wkn.swap02⟩
+
+@[simp]
+theorem InS.coe_swap02 {first second third : Ty α × ε} {Γ : Ctx α ε}
+  : (InS.swap02 (Γ := Γ) (first := first) (second := second) (third := third) : ℕ → ℕ) = Nat.swap0 2
+  := rfl
+
 @[simp]
 theorem Wkn.add2 {first second} {Γ : Ctx α ε}
   : Wkn (first::second::Γ) Γ (· + 2)

DeBruijnSSA/BinSyntax/Typing/Term/Subst.lean

@@ -276,3 +276,11 @@ theorem InS.subst0_var0_wk1 {Γ : Ctx α ε}
 theorem InS.subst0_wk0 {Γ : Ctx α ε}
   (a : InS φ Γ V) (b : InS φ Γ V') : a.wk0.subst b.subst0 = a
   := by ext; simp
+
+def Subst.InS.fromWk {Γ Δ : Ctx α ε} (h : Γ.InS Δ) : Subst.InS φ Γ Δ
+  := ⟨Subst.fromWk h, λi => by simp only [Set.mem_setOf_eq, fromWk_apply, Wf.var_iff, h.prop i]⟩
+
+@[simp]
+theorem Subst.InS.coe_fromWk {Γ Δ : Ctx α ε} (h : Γ.InS Δ)
+  : ((fromWk h : Subst.InS φ Γ Δ) : Subst φ) = Subst.fromWk h
+  := rfl