Proofgold Proof

pf
Let x0 of type ι be given. Let x1 of type ι be given. Assume H0: prim1 x1 x0. Apply orIL with prim1 x1 x0, and (empty_p x0) (empty_p x1). The subproof is completed by applying H0. ■