Proofgold Proof

pf
Let x0 of type ι → ο be given. Assume H0: x0 5e331... Assume H1: ∀ x1 x2 . x0 x1 ⟶ x0 x2 ⟶ x0 (a3eb9.. x1 x2). Assume H2: ∀ x1 x2 . x0 x1 ⟶ x0 x2 ⟶ x0 (bf68c.. x1 x2). The subproof is completed by applying H0. ■