Let x0 of type ι be given.
Apply unknownprop_5cf7e6965e83150a1907c25d96a0fc30a3e05ee07284c284a3b5f6261ce28afc with
λ x1 x2 . 236dc.. (bc82c.. (ce322.. x0) x2) (bc82c.. (f6a32.. x0) (f6a32.. 4a7ef..)) = x0.
Apply unknownprop_116b1a7b5ba65ca627825e84d83931af55cf809780b181dd0b77c132ec226190 with
λ x1 x2 . 236dc.. (bc82c.. (ce322.. x0) 4a7ef..) (bc82c.. (f6a32.. x0) x2) = x0.
Apply unknownprop_3201a7f403ac32d9752260880c29e9f9084a9b6a0cf9218208744c4c82940cb1 with
ce322.. x0,
λ x1 x2 . 236dc.. x2 (bc82c.. (f6a32.. x0) 4a7ef..) = x0 leaving 2 subgoals.
Apply unknownprop_c50e383ae63caacff66491342f6a1cc504e440cc936d7430270036bd6758f48a with
x0.
The subproof is completed by applying H0.
Apply unknownprop_3201a7f403ac32d9752260880c29e9f9084a9b6a0cf9218208744c4c82940cb1 with
f6a32.. x0,
λ x1 x2 . 236dc.. (ce322.. x0) x2 = x0 leaving 2 subgoals.
Apply unknownprop_29514e25826fa0a942e92f047f92b24dd63fba7537353bf59d9f591e0be2370c with
x0.
The subproof is completed by applying H0.
Let x1 of type ι → ι → ο be given.
Apply unknownprop_5bfa7e2c4e0c8770e52c317d4111804765880efbe213ccc7f49552da8205fc8a with
x0,
λ x2 x3 . x1 x3 x2.
The subproof is completed by applying H0.