simp only [occursFreeIn]
case a.h.a.h1.a
D : Type
I : Interpretation D
phi psi : 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)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
v : Var
a1 : occursFreeIn v phi
⊢ occursFreeIn v (phi.imp_ psi)
case a.h.a.h1.a
D : Type
I : Interpretation D
phi psi : 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)
psi_ih :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v psi → V v = V' v) → (Holds D I V psi ↔ Holds D I V' psi)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (phi.imp_ psi) → V v = V' v
v : Var
a1 : occursFreeIn v phi
⊢ occursFreeIn v phi ∨ occursFreeIn v psi