Let x0 of type ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
proj0 x0,
ap x0 0 leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_5790343a8368d4f3aa514e68a19a3e4824006be2aed8a0a7a707f542e4c79154 with
x0,
0,
x1.
Apply unknownprop_5992b8b7bec7fb836d55125523d586d30ffbc11c7b85cf6cd43502369de91721 with
x0,
x1.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H0:
In x1 (ap x0 0).
Apply unknownprop_ceb85c7fe43781527455d6fbd821c5b30186b44a5471ea98652de6fa2b7064d9 with
x0,
x1.
Apply unknownprop_762358d061bd2484ba81471a0b72cf827e125ecce5f1471d9abb4ee5039695f2 with
x0,
0,
x1.
The subproof is completed by applying H0.