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.. (ce322.. x0) x2) (bc82c.. (f6a32.. x0) (f6a32.. (236dc.. (f4dc0.. (ce322.. x0)) (f4dc0.. (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.. (ce322.. x0) (f4dc0.. (ce322.. x0))) (bc82c.. (f6a32.. x0) x2) = 4a7ef.. leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
Apply unknownprop_5cbe8643f1e45151334fcd7208ed4c5dc2b120486b5022cdc81170c910647c5d with
ce322.. x0,
λ x1 x2 . 236dc.. x2 (bc82c.. (f6a32.. x0) (f4dc0.. (f6a32.. x0))) = 4a7ef.. leaving 2 subgoals.
Apply unknownprop_c50e383ae63caacff66491342f6a1cc504e440cc936d7430270036bd6758f48a with
x0.
The subproof is completed by applying H0.
Apply unknownprop_5cbe8643f1e45151334fcd7208ed4c5dc2b120486b5022cdc81170c910647c5d 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...