case pred_2 h1_Γ h1_Δ h1_phi h1_x h1_1 h1_2 =>
  have s1 : IsNotFree D I M E h1_phi h1_x
  apply not_free_imp_is_not_free D I M E h1_phi h1_Γ h1_x h1_2
  exact nf h1_x
  simp only [Holds]
  intro V a1 a
  unfold IsNotFree at s1
  simp only [← s1 V a]
  exact a1
D : Type
I : Interpretation D
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h2 : E.WellFormed
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi : Formula
h1_x : VarName
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : NotFree h1_Γ h1_x h1_phi
M : MetaValuation D
nf : ∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v
hyp : ∀ (F : Formula) (V : Valuation D), F ∈ h1_Δ → Holds D I V M E F
⊢ ∀ (V : Valuation D), Holds D I V M E (h1_phi.imp_ (forall_ h1_x h1_phi))
no goals