Let x0 of type ι be given.
Apply unknownprop_d74508268cf2245bb4de852843c85bf4733bd48f6383eaac9c68dfae0d149115 with
707e2.. (4326e.. x0),
x0.
Let x1 of type ι be given.
Apply iffI with
prim1 x1 (707e2.. (4326e.. x0)),
prim1 x1 x0 leaving 2 subgoals.
Apply unknownprop_381047c913ae030e9e9942d1a8901abc4d96b713731a5b7b04cd06cd75bdfe7a with
4326e.. x0,
x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_87135efbd349f82ea798668ead3e3c95927d5ac9bf1fcb9052c1dff107e96de8 with x0.
The subproof is completed by applying H1.
Apply unknownprop_81e2497d53f26977fa8ca722fab407ecbd3aa74818556ba29653e265699cc106 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L2.
Apply unknownprop_ef71c7659631e6712550b179497e8718243f15729bbc2ba1fccf8bb659c5df87 with
4326e.. x0,
x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_87135efbd349f82ea798668ead3e3c95927d5ac9bf1fcb9052c1dff107e96de8 with x0.
Apply unknownprop_547d526f8f61234c156e3c73fa4a8a1aa9a628b58fe16fb380304ebbca858804 with
x0,
x1.
The subproof is completed by applying H1.