case forall_ x phi phi_ih =>
  unfold Formula.metaVarSet at h1
  simp only [Holds]
  apply forall_congr'
  intro a
  exact phi_ih (Function.updateITE V x a) M M' 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)
x : VarName
phi : 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)
V : Valuation D
M M' : MetaValuation D
h1 : ∀ (V' : Valuation D), ∀ X ∈ (forall_ x phi).metaVarSet, M X V' ↔ M' X V'
⊢ Holds D I V M (head✝ :: tail✝) (forall_ x phi) ↔ Holds D I V M' (head✝ :: tail✝) (forall_ x phi)
no goals