exact a1
case a
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
x : String
a1 : occursFreeIn (free_ x) phi
⊢ occursFreeIn (lift (free_ x)) phi
no goals