Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_ddfc870a0f67dd8bf5406d70b56c890bf0a0c8baf75fc04a131d801e13a59627 with
2,
x0,
x1 leaving 4 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying In_1_2.
Apply unknownprop_a4edcbab661199d6911d1441c90756c844d60baa5bb17d517bccec0c64f7803b with
x0,
2.
The subproof is completed by applying H0.
The subproof is completed by applying H1.