case thm h1_Γ h1_Γ' h1_Δ h1_Δ' h1_phi h1_σ h1_τ h1_1 h1_2 h1_3 h1_4 h1_ih_1 h1_ih_2 =>
  exact lem_2_a E h1_σ h1_τ h1_phi h1_ih_2 h1_1
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ h1_Γ' : List (VarName × MetaVarName)
h1_Δ h1_Δ' : List Formula
h1_phi : Formula
h1_σ : Instantiation
h1_τ : MetaInstantiation
h1_1 : ∀ X ∈ h1_phi.metaVarSet, IsMetaVarOrAllDefInEnv E (h1_τ X)
h1_2 : ∀ (x : VarName) (X : MetaVarName), (x, X) ∈ h1_Γ → NotFree h1_Γ' (↑h1_σ x) (h1_τ X)
h1_3 : ∀ psi ∈ h1_Δ, IsProof E h1_Γ' h1_Δ' (sub h1_σ h1_τ psi)
h1_4 : IsProof E h1_Γ h1_Δ h1_phi
h1_ih_1 : ∀ psi ∈ h1_Δ, IsMetaVarOrAllDefInEnv E (sub h1_σ h1_τ psi)
h1_ih_2 : IsMetaVarOrAllDefInEnv E h1_phi
⊢ IsMetaVarOrAllDefInEnv E (sub h1_σ h1_τ h1_phi)
no goals