Let x0 of type ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
proj1 x0,
ap x0 1 leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_5790343a8368d4f3aa514e68a19a3e4824006be2aed8a0a7a707f542e4c79154 with
x0,
1,
x1.
Apply unknownprop_ddee32b485fe3b18e7ed6649c430b0ba07fbbe95c6ca01a1512260320292f5d6 with
x0,
x1.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H0:
In x1 (ap x0 1).
Apply unknownprop_83b1431ffbe4fafc920badacc16dca6e556c4f5636fd99bcf3d43ceb7144eaab with
x0,
x1.
Apply unknownprop_762358d061bd2484ba81471a0b72cf827e125ecce5f1471d9abb4ee5039695f2 with
x0,
1,
x1.
The subproof is completed by applying H0.