repeat first | constructor | assumption
E : Env
Γ : List (VarName × MetaVarName)
Δ : List Formula
F : Formula
h1_Γ : List (VarName × MetaVarName)
h1_Δ : List Formula
h1_x h1_y h1_z : VarName
⊢ IsMetaVarOrAllDefInEnv E (eq_ h1_x h1_y) ∧ IsMetaVarOrAllDefInEnv E ((eq_ h1_x h1_z).imp_ (eq_ h1_y h1_z))
no goals