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