Proofgold Proof

pf

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

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

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

■