Let x0 of type ι be given.
Apply unknownprop_2c27682abc32e1c8a2160a07043a81afe1f256df4f0472edf3cf11efdcea8609 with
x0,
e4431.. x0 = x0 leaving 2 subgoals.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_58b9911fe66d684a6d40350a803ba9ad994b8c3fb391c59cf63767464366ef65 with
x0,
e4431.. x0,
x0 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply unknownprop_e9e7859de6407ac534393134c6baa6d21f37ec1709d7126bcb1293f7feedcd5f with
x0.
The subproof is completed by applying H0.