congr! 1
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
psi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
V : VarAssignment D
⊢ (Holds D I (V ∘ σ) E phi ↔ Holds D I (V ∘ σ) E psi) ↔
    (Holds D I V E (replaceAll σ phi) ↔ Holds D I V E (replaceAll σ psi))
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
psi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)

case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
psi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)