exact h1_ih_2_right
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
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 h1_ih_2_left : IsMetaVarOrAllDefInEnv E h1_phi
h1_ih_2_right : IsMetaVarOrAllDefInEnv E h1_psi
⊢ IsMetaVarOrAllDefInEnv E h1_psi
no goals