Let x0 of type ι be given.
Apply unknownprop_2c27682abc32e1c8a2160a07043a81afe1f256df4f0472edf3cf11efdcea8609 with
x0,
prim1 x0 (56ded.. (4ae4a.. (e4431.. x0))) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_5a5c48612170d465714265799d25003db15da4f2d5d05eaf9fa403276d7d9f0a with
4ae4a.. (e4431.. x0),
x0,
e4431.. x0 leaving 3 subgoals.
Apply unknownprop_1f03c3e4cc230143731a84d6351b78522f6051d5113f644774435abf9cb5a984 with
e4431.. x0.
The subproof is completed by applying H1.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with
e4431.. x0.
The subproof is completed by applying H2.