congr!
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ (sub τ phi).iff_ (sub τ psi) = phi.iff_ psi
case h.e'_1
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ sub τ phi = phi

case h.e'_2
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ sub τ psi = psi