case mp h1_Γ h1_Δ h1_phi h1_psi h1_1 h1_2 h1_ih_1 h1_ih_2 =>
  simp only [Holds] at h1_ih_2
  intro V
  exact h1_ih_2 M nf hyp V (h1_ih_1 M nf hyp V)
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 h1_psi : Formula
h1_1 : IsProof E h1_Γ h1_Δ h1_phi
h1_2 : IsProof E h1_Γ h1_Δ (h1_phi.imp_ h1_psi)
h1_ih_1 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (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
h1_ih_2 :
  ∀ (M : MetaValuation D),
    (∀ (v : VarName) (X : MetaVarName), (v, X) ∈ h1_Γ → IsNotFree D I M E (meta_var_ X) v) →
      (∀ (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_ h1_psi)
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_psi
no goals