Proofgold Term Root Disambiguation

∀ x0 : ι → ι → ο . trichotomous_or_i x0 ⟶ ∀ x1 x2 . or (or (x0 x1 x2) (x1 = x2)) (x0 x2 x1)

as obj
-

as prop
a26a2..^{trichotomous_or_i_E}

theory
HF

stx
b6147..

address
TMKAh..^{trichotomous_or_i_E}