Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
SNoElts_ x0,
SNoElts_ x1.
Apply unknownprop_023b2e512ed9c52f995f2d07c1a06cfb4ae27f29745759c860f7e880eac7d40f with
x0,
λ x2 . In x2 (SNoElts_ x1) leaving 2 subgoals.
Let x2 of type ι be given.
Apply unknownprop_61a2d0a1af971a8a33860a80d37d54af6bb47fdbde7cb51745bdfe9c90bba67d with
x1,
x2.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Apply unknownprop_e43b40f457d85ed5127565f4d10d01301fdebb1a0abdb4f8f1ca4edd08e1458f with
x1,
x2.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.