Apply unknownprop_8e364bf141acac18f61b9e8282040b72d6b420e48399109d2ed0181edd60c3f3 with λ x1 x2 : (ι → ι → ο) → ο . strictpartialorder_ix0 ⟶ trichotomous_or_ix0 ⟶ x2x0.
The subproof is completed by applying unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with strictpartialorder_ix0, trichotomous_or_ix0.