Let x0 of type ι be given.
Apply unknownprop_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with
ce322.. x0.
Apply unknownprop_c50e383ae63caacff66491342f6a1cc504e440cc936d7430270036bd6758f48a with
x0.
The subproof is completed by applying H0.
Apply unknownprop_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with
f6a32.. x0.
Apply unknownprop_29514e25826fa0a942e92f047f92b24dd63fba7537353bf59d9f591e0be2370c with
x0.
The subproof is completed by applying H0.
Apply unknownprop_af5a8211ff947ff893b5035a5559a8e74e1503a79511eecb1f7a8d29e2eae278 with
f4dc0.. (ce322.. x0),
f4dc0.. (f6a32.. x0),
λ x1 x2 . 236dc.. (bc82c.. x2 (ce322.. x0)) (bc82c.. (f6a32.. (236dc.. (f4dc0.. (ce322.. x0)) (f4dc0.. (f6a32.. x0)))) (f6a32.. x0)) = 4a7ef.. leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
Apply unknownprop_23664dbeb9b115697e6a9c597ef741d81e66962cba0c9c5f51bdcd68c09e293f with
f4dc0.. (ce322.. x0),
f4dc0.. (f6a32.. x0),
λ x1 x2 . 236dc.. (bc82c.. (f4dc0.. (ce322.. x0)) (ce322.. x0)) (bc82c.. x2 (f6a32.. x0)) = 4a7ef.. leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
Apply unknownprop_e9028cba89e89a77a2997386e65c0b630a8780de144826d2529038cff74afa4d with
ce322.. x0,
λ x1 x2 . 236dc.. x2 (bc82c.. (f4dc0.. (f6a32.. x0)) (f6a32.. x0)) = 4a7ef.. leaving 2 subgoals.
Apply unknownprop_c50e383ae63caacff66491342f6a1cc504e440cc936d7430270036bd6758f48a with
x0.
The subproof is completed by applying H0.
Apply unknownprop_e9028cba89e89a77a2997386e65c0b630a8780de144826d2529038cff74afa4d with
f6a32.. x0,
λ x1 x2 . 236dc.. 4a7ef.. x2 = 4a7ef.. leaving 2 subgoals.
Apply unknownprop_29514e25826fa0a942e92f047f92b24dd63fba7537353bf59d9f591e0be2370c with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_8caab58746e5d2d24e79c56b1fd1ad38271bed0128653f24088edadc36aa9114 with
4a7ef...