Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: ordinal x0. Let x1 of type ι be given. Assume H1: 1beb9.. x0 x1. Let x2 of type ο be given. Assume H2: ∀ x3 . and (ordinal x3) (1beb9.. x3 x1) ⟶ x2. Apply H2 with x0. Apply andI with ordinal x0, 1beb9.. x0 x1 leaving 2 subgoals. The subproof is completed by applying H0. The subproof is completed by applying H1. ■