Proofgold Proof

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