Proofgold Proof

pf
Apply UnivOf_TransSet with prim6 0, prim6 0, 1 leaving 2 subgoals. The subproof is completed by applying UnivOf_In with prim6 0. Apply nat_p_UnivOf_Empty with 1. The subproof is completed by applying nat_1. ■