Apply unknownprop_593fa0231131d03f1c1318f5378e70a45001b6bbcae8d713cdb3ec5c8fae3570 with
4a7ef...
Let x0 of type ι be given.
Apply FalseE with
80242.. x0.
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with
x0.
The subproof is completed by applying H0.