Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with
x0.
The subproof is completed by applying H0.
Apply unknownprop_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with
x1.
The subproof is completed by applying H1.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_5cbe8643f1e45151334fcd7208ed4c5dc2b120486b5022cdc81170c910647c5d with
bc82c.. x0 x1,
λ x2 x3 . x3 = bc82c.. (bc82c.. x0 x1) (bc82c.. (f4dc0.. x0) (f4dc0.. x1)) leaving 2 subgoals.
The subproof is completed by applying L4.
Apply unknownprop_d8f468fc749efab866c779febbe4cd601b5e2eeaa90e3f207f17de20f4ab68ab with
bc82c.. x0 x1,
f4dc0.. x0,
f4dc0.. x1,
λ x2 x3 . 4a7ef.. = x3 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply unknownprop_443bf25288cf39bc78395680f7fe50ad1a2a509c594b439821412f6af4f99866 with
x0,
x1,
λ x2 x3 . 4a7ef.. = bc82c.. (bc82c.. x3 (f4dc0.. x0)) (f4dc0.. x1) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_d8f468fc749efab866c779febbe4cd601b5e2eeaa90e3f207f17de20f4ab68ab with
x1,
x0,
f4dc0.. x0,
λ x2 x3 . 4a7ef.. = bc82c.. x2 (f4dc0.. x1) leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying L2.
Apply unknownprop_5cbe8643f1e45151334fcd7208ed4c5dc2b120486b5022cdc81170c910647c5d with
x0,
λ x2 x3 . 4a7ef.. = bc82c.. (bc82c.. x1 x3) (f4dc0.. x1) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_3201a7f403ac32d9752260880c29e9f9084a9b6a0cf9218208744c4c82940cb1 with
x1,
λ x2 x3 . 4a7ef.. = bc82c.. x3 (f4dc0.. x1) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_5cbe8643f1e45151334fcd7208ed4c5dc2b120486b5022cdc81170c910647c5d with
x1,
λ x2 x3 . 4a7ef.. = x3 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H5.
Apply unknownprop_dff6e8fda85df9e92da1fa7de32e7db4e93608d23c35200508d6d4985bb05bac with
bc82c.. x0 x1,
f4dc0.. (bc82c.. x0 x1),
bc82c.. (f4dc0.. x0) (f4dc0.. x1) leaving 4 subgoals.
The subproof is completed by applying L4.
Apply unknownprop_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with
bc82c.. x0 x1.
The subproof is completed by applying L4.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with
f4dc0.. x0,
f4dc0.. x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
The subproof is completed by applying L5.