An exact proof term for the current goal is (or3E (alpha ∈ beta) (alpha = beta) (beta ∈ alpha) (ordinal_trichotomy_or alpha beta H1 H2)).