cases h1
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
h1 : phi.metaVarSet = ∅ ∧ psi.metaVarSet = ∅
⊢ (sub σ τ phi).imp_ (sub σ τ psi) = (sub σ τ' phi).imp_ (sub σ τ' psi)
case intro
σ : Instantiation
τ τ' : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → sub σ τ phi = sub σ τ' phi
psi_ih : psi.metaVarSet = ∅ → sub σ τ psi = sub σ τ' psi
left✝ : phi.metaVarSet = ∅
right✝ : psi.metaVarSet = ∅
⊢ (sub σ τ phi).imp_ (sub σ τ psi) = (sub σ τ' phi).imp_ (sub σ τ' psi)