Proofgold Proof

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