Apply nat_p_UnivOf_Empty with
1.
The subproof is completed by applying nat_1.
Apply nat_p_UnivOf_Empty with
2.
The subproof is completed by applying nat_2.
Apply unknownprop_b1a3c96c449f03f4a28581f6960a1c83d6c7a078ae9a00e66ef3586912ebf9b3 with
λ x0 . x0 ∈ prim6 0 leaving 2 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.