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