exact psi_ih h1_right
case h.e'_2
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ sub σ τ psi = sub σ τ' psi
no goals