Let x0 of type ι be given.
Apply unknownprop_5cf7e6965e83150a1907c25d96a0fc30a3e05ee07284c284a3b5f6261ce28afc with
λ x1 x2 . 236dc.. (bc82c.. x2 (ce322.. x0)) (bc82c.. (f6a32.. 4a7ef..) (f6a32.. x0)) = x0.
Apply unknownprop_116b1a7b5ba65ca627825e84d83931af55cf809780b181dd0b77c132ec226190 with
λ x1 x2 . 236dc.. (bc82c.. 4a7ef.. (ce322.. x0)) (bc82c.. x2 (f6a32.. x0)) = x0.
Apply unknownprop_ccff4249496414413c3c95467fb8c02c96509ca2826dc03833e7de26e75fcd74 with
ce322.. x0,
λ x1 x2 . 236dc.. x2 (bc82c.. 4a7ef.. (f6a32.. x0)) = x0 leaving 2 subgoals.
Apply unknownprop_c50e383ae63caacff66491342f6a1cc504e440cc936d7430270036bd6758f48a with
x0.
The subproof is completed by applying H0.
Apply unknownprop_ccff4249496414413c3c95467fb8c02c96509ca2826dc03833e7de26e75fcd74 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.