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