Let x0 of type ι be given.
Let x1 of type ι be given.
Apply set_ext with
d3786.. x0 x1,
d3786.. x1 x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_b20a00aa87d496967e8437c14db8d889fd9e9e9d5d666566fec11b526658d264 with x0, x1.
The subproof is completed by applying unknownprop_b20a00aa87d496967e8437c14db8d889fd9e9e9d5d666566fec11b526658d264 with x1, x0.