simp only [shift]
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (free_ x) = shift D V d (free_ x)
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
x : String
⊢ (V ∘ Var.openList j (List.map free_ zs)) (free_ x) = V (free_ x)