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