Let x0 of type ι be given.
Apply set_ext with
1ad11.. x0 4a7ef..,
x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_f4cb3db9b44278d291dda59763d3ebc8189ce94e5657538eeb63abd989060e4e with
x0,
4a7ef...
Let x1 of type ι be given.
Apply unknownprop_4469442df960b88f16925ae745a59dde3c3d26a1d7b003702e92e0a7ea2361ef with
x0,
4a7ef..,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with x1.