Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply H1 leaving 2 subgoals.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
x2 = x0.
Assume H2: x2 = x0.
Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with
x2,
UPair x0 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply H2 with
λ x3 x4 . In x4 (UPair x0 x1).
The subproof is completed by applying unknownprop_f40d13744d00ec34b223eab4c005556ef718e0ee3d9e509403edfd952d571ca0 with x0, x1.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with
x2 = x1.
Assume H2: x2 = x1.
Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with
x2,
UPair x0 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply H2 with
λ x3 x4 . In x4 (UPair x0 x1).
The subproof is completed by applying unknownprop_062c64c10c58e9562a87a79165ec64b8525d3f91b15ae8561687c786947b4cb0 with x0, x1.