Apply unknownprop_39316ce080d87a012ee204f2ac1804587ff42553ad17dbec781a566574cc2a25 with
λ x0 . x0 ∈ prim6 (prim6 0) leaving 2 subgoals.
The subproof is completed by applying unknownprop_2d528c4139c2d1dd93298c1a64e321954c834d3f235fb8de989a2b5f9826cd01.
The subproof is completed by applying unknownprop_b89e3967a5c3d507a04eb70fb2dec2dc464e0e30b824990a36892573b7bd98c0.