cases 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
case h.h1.free_
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
a✝ : String
a1 : occursFreeIn (free_ a✝) phi
⊢ shift D V d (free_ a✝) = shift D V' d (free_ a✝)

case h.h1.bound_
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
a✝ : ℕ
a1 : occursFreeIn (bound_ a✝) phi
⊢ shift D V d (bound_ a✝) = shift D V' d (bound_ a✝)