Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with
x0.
The subproof is completed by applying H0.
Apply unknownprop_d8f468fc749efab866c779febbe4cd601b5e2eeaa90e3f207f17de20f4ab68ab with
f4dc0.. x0,
x0,
x1,
λ x3 x4 . x4 = x1 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_e9028cba89e89a77a2997386e65c0b630a8780de144826d2529038cff74afa4d with
x0,
λ x3 x4 . bc82c.. x4 x1 = x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_ccff4249496414413c3c95467fb8c02c96509ca2826dc03833e7de26e75fcd74 with
x1.
The subproof is completed by applying H1.
Apply unknownprop_d8f468fc749efab866c779febbe4cd601b5e2eeaa90e3f207f17de20f4ab68ab with
f4dc0.. x0,
x0,
x2,
λ x3 x4 . x4 = x2 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_e9028cba89e89a77a2997386e65c0b630a8780de144826d2529038cff74afa4d with
x0,
λ x3 x4 . bc82c.. x4 x2 = x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_ccff4249496414413c3c95467fb8c02c96509ca2826dc03833e7de26e75fcd74 with
x2.
The subproof is completed by applying H2.
Apply L5 with
λ x3 x4 . x3 = x2.
Apply H3 with
λ x3 x4 . bc82c.. (f4dc0.. x0) x4 = x2.
The subproof is completed by applying L6.