Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_d8f468fc749efab866c779febbe4cd601b5e2eeaa90e3f207f17de20f4ab68ab with
x0,
f4dc0.. x0,
x1,
λ x2 x3 . x3 = x1 leaving 4 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_5cbe8643f1e45151334fcd7208ed4c5dc2b120486b5022cdc81170c910647c5d 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.