unfold Formula.metaVarSet at h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ (phi.imp_ psi).metaVarSet, M X V' ↔ M' X V'
⊢ Holds D I V M (head✝ :: tail✝) (phi.imp_ psi) ↔ Holds D I V M' (head✝ :: tail✝) (phi.imp_ psi)
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : Valuation D) (M M' : MetaValuation D) (F : Formula),
    (∀ (V' : Valuation D), ∀ X ∈ F.metaVarSet, M X V' ↔ M' X V') → (Holds D I V M tail✝ F ↔ Holds D I V M' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) phi ↔ Holds D I V M' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : Valuation D) (M M' : MetaValuation D),
    (∀ (V' : Valuation D), ∀ X ∈ psi.metaVarSet, M X V' ↔ M' X V') →
      (Holds D I V M (head✝ :: tail✝) psi ↔ Holds D I V M' (head✝ :: tail✝) psi)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ phi.metaVarSet ∪ psi.metaVarSet, M X V' ↔ M' X V'
⊢ Holds D I V M (head✝ :: tail✝) (phi.imp_ psi) ↔ Holds D I V M' (head✝ :: tail✝) (phi.imp_ psi)