simp
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → psi.metaVarSet = ∅
vs : List VarName
h1_left : NoMetaVarAndAllFreeInList vs phi
h1_right : NoMetaVarAndAllFreeInList vs psi
⊢ ∅ ∪ ∅ = ∅
no goals