Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_ddfc870a0f67dd8bf5406d70b56c890bf0a0c8baf75fc04a131d801e13a59627 with
3,
binunion x0 {(λ x5 . SetAdjoin x5 (Sing 2)) x4|x4 ∈ x1},
x2 leaving 4 subgoals.
The subproof is completed by applying nat_3.
The subproof is completed by applying In_1_3.
Apply unknownprop_d70cc86669636f09f3d7916eef547e3c121ef7467f1e4baa7bd1bb2d082b0fbe with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_ddfc870a0f67dd8bf5406d70b56c890bf0a0c8baf75fc04a131d801e13a59627 with
4,
binunion (binunion x0 {(λ x5 . SetAdjoin x5 (Sing 2)) x4|x4 ∈ x1}) {(λ x5 . SetAdjoin x5 (Sing 3)) x4|x4 ∈ x2},
x3 leaving 4 subgoals.
The subproof is completed by applying nat_4.
The subproof is completed by applying In_1_4.
The subproof is completed by applying L4.
The subproof is completed by applying H3.