Apply unknownprop_527cc5ff4380236ca54e2a0208bde8411cd2e1124e14f7764871099a03bebf91 with
prim6 (prim6 0) leaving 2 subgoals.
The subproof is completed by applying UnivOf_TransSet with
prim6 0.
The subproof is completed by applying UnivOf_ZF_closed with
prim6 0.
Apply unknownprop_7e80016cd90eba8cfb22e412d51217cbc5f2eeece9405f5140e2181ec01c4b9a with
λ x0 . x0 ∈ prim6 (prim6 0).
The subproof is completed by applying L0.