Proofgold Proof

pf

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

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

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

■