Proofgold Proof

pf
Apply and_def with λ x0 x1 : ο → ο → ο . ∀ x2 x3 : ο . x1 x2 x3 ⟶ ∀ x4 : ο . (x2 ⟶ x3 ⟶ x4) ⟶ x4. Let x0 of type ο be given. Let x1 of type ο be given. Assume H0: ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2. The subproof is completed by applying H0. ■