simp
case s1.left
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ v ∈ phi.freeVarSet \ {x}
case s1.left
D : Type
I : Interpretation D
E : Env
c : Char
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
d : D
v : VarName
a1 : isFreeIn v phi
c1 : ¬∃ y ∈ phi.freeVarSet \ {x}, σ y = x
c2 : ¬v = x
contra : σ v = x
⊢ v ∈ phi.freeVarSet ∧ ¬v = x