case intro h2_left h2_right =>
  unfold sub
  simp only [Holds]
  apply forall_congr'
  intro a
  have s1 : Function.updateITE V (σ.val x) a ∘ σ.val = Function.updateITE (V ∘ σ.val) x a
  apply Function.updateITE_comp_right_injective
  apply Instantiation.is_injective
  simp only [← s1]
  exact phi_ih (Function.updateITE V (σ.val x) a) h1
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
σ : Instantiation
σ' : VarName → VarName
τ : MetaInstantiation
x : VarName
phi : Formula
phi_ih :
  ∀ (V : Valuation D),
    IsMetaVarOrAllDefInEnv E phi →
      (Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E phi ↔ Holds D I V M E (sub σ τ phi))
V : Valuation D
h1 : IsMetaVarOrAllDefInEnv E phi
h2_left : ↑σ ∘ σ' = id
h2_right : σ' ∘ ↑σ = id
⊢ Holds D I (V ∘ ↑σ) (fun X' V' => Holds D I (V' ∘ σ') M E (τ X')) E (forall_ x phi) ↔
    Holds D I V M E (sub σ τ (forall_ x phi))
no goals