simp only [sub]
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (phi.iff_ psi)) ↔ Holds D I (V ∘ σ) E (phi.iff_ psi)
D : Type
I : Interpretation D
E : Env
c : Char
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
psi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c psi) ↔ Holds D I (V ∘ σ) E psi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E ((sub σ c phi).iff_ (sub σ c psi)) ↔ Holds D I (V ∘ σ) E (phi.iff_ psi)