Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
2,
UPair 0 1.
Let x0 of type ι be given.
Apply unknownprop_84fe37a922385756a4e0826a593defb788cadbe4bdc9a7fe6b519ea49f509df5 with
1,
x0,
In x0 (UPair 0 1) leaving 3 subgoals.
The subproof is completed by applying H0.
Claim L2: x0 = 0
Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with
0,
x0.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
1,
Sing 0,
x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_e8598561026ee5bf15479322ab1713bd41b786cd16638ceaff374ea0aee3dd94.
The subproof is completed by applying H1.
Apply L2 with
λ x1 x2 . In x2 (UPair 0 1).
The subproof is completed by applying unknownprop_f40d13744d00ec34b223eab4c005556ef718e0ee3d9e509403edfd952d571ca0 with 0, 1.
Assume H1: x0 = 1.
Apply H1 with
λ x1 x2 . In x2 (UPair 0 1).
The subproof is completed by applying unknownprop_062c64c10c58e9562a87a79165ec64b8525d3f91b15ae8561687c786947b4cb0 with 0, 1.