Proofgold Proof

pf
Let x0 of type ι → ι → ο be given. Apply unknownprop_8e364bf141acac18f61b9e8282040b72d6b420e48399109d2ed0181edd60c3f3 with λ x1 x2 : (ι → ι → ο) → ο . x2 x0 ⟶ ∀ x3 : ο . (strictpartialorder_i x0 ⟶ trichotomous_or_i x0 ⟶ x3) ⟶ x3. The subproof is completed by applying andE with strictpartialorder_i x0, trichotomous_or_i x0. ■