Proofgold Proof

pf

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

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

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

■