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