Let x0 of type ι be given.
Apply unknownprop_8fbd0c2b48e78882e15936a0ad5f4a3c5af2cb37d9320d8cb210a91462e202ca with
x0.
The subproof is completed by applying H0.
Apply unknownprop_443bf25288cf39bc78395680f7fe50ad1a2a509c594b439821412f6af4f99866 with
x0,
f4dc0.. x0,
λ x1 x2 . x2 = 4a7ef.. leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L1.
Apply unknownprop_e9028cba89e89a77a2997386e65c0b630a8780de144826d2529038cff74afa4d with
x0.
The subproof is completed by applying H0.