funext v
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
⊢ shift D V d ∘ Var.close (j + 1) (free_ z) = shift D (V ∘ Var.close j (free_ z)) d
case h
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
v : Var
⊢ (shift D V d ∘ Var.close (j + 1) (free_ z)) v = shift D (V ∘ Var.close j (free_ z)) d v