simp only [Finset.union_eq_empty] at 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_ psi) = sub σ τ' (phi.imp_ psi)
σ : 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_ psi) = sub σ τ' (phi.imp_ psi)