Proofgold Proof

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