constructor
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet = ∅ ∧ (sub σ τ psi).metaVarSet = ∅
case left
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ (sub σ τ phi).metaVarSet = ∅

case right
σ : Instantiation
τ : MetaInstantiation
phi psi : Formula
phi_ih : phi.metaVarSet = ∅ → (sub σ τ phi).metaVarSet = ∅
psi_ih : psi.metaVarSet = ∅ → (sub σ τ psi).metaVarSet = ∅
h1_left : phi.metaVarSet = ∅
h1_right : psi.metaVarSet = ∅
⊢ (sub σ τ psi).metaVarSet = ∅