Proofgold Proof

pf

Let x0 of type ι → ι → ο be given.

Apply unknownprop_5cef9e5da65ddd9e109279d054792510e640b761edb0ef1727132ba3831beaab with λ x1 x2 : (ι → ι → ο) → ο . x2 x0 ⟶ ∀ x3 : ο . (reflexive_i x0 ⟶ symmetric_i x0 ⟶ transitive_i x0 ⟶ x3) ⟶ x3.

The subproof is completed by applying unknownprop_1eb28f5831a9d21e218b89c238edbbf849d22045bb77ce7cec926a651d1793f0 with reflexive_i x0, symmetric_i x0, transitive_i x0.

■