case prop_2 h1_Γ h1_Δ h1_phi h1_psi h1_chi h1_1 h1_2 h1_3 =>
  repeat first | constructor | assumption
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_phi h1_psi h1_chi : Formula
h1_1 : IsMetaVarOrAllDefInEnv E h1_phi
h1_2 : IsMetaVarOrAllDefInEnv E h1_psi
h1_3 : IsMetaVarOrAllDefInEnv E h1_chi
⊢ IsMetaVarOrAllDefInEnv E ((h1_phi.imp_ (h1_psi.imp_ h1_chi)).imp_ ((h1_phi.imp_ h1_psi).imp_ (h1_phi.imp_ h1_chi)))
no goals