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