Proofgold Proof

pf
Let x0 of type ι → ο be given. Let x1 of type ι be given. Assume H0: ∀ x2 . x0 x2. Assume H1: x0 x1 ⟶ False. Apply H1. The subproof is completed by applying H0 with x1. ■