intro v a1
case h.h1
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
⊢ ∀ (v : Var), occursFreeIn v phi → shift D V d v = shift D V' d v
case h.h1
D : Type
I : Interpretation D
x : String
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v phi → V v = V' v) → (Holds D I V phi ↔ Holds D I V' phi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn (lift v) phi → V v = V' v
d : D
v : Var
a1 : occursFreeIn v phi
⊢ shift D V d v = shift D V' d v