Proofgold Proof

pf
Let x0 of type ι → ι → ο be given. Assume H0: and (symmetric x0) (transitive x0). Apply andER with symmetric x0, transitive x0. The subproof is completed by applying H0. ■