Let x0 of type ι be given.
Let x1 of type ι be given.
Apply set_ext with
22ca9.. (aae7a.. x0 x1),
x1 leaving 2 subgoals.
Let x2 of type ι be given.
Apply unknownprop_b99ca2c7d71b08f49bc694a4f2f3716eab3cfc0a3351cd23d1373c39bcb2b95c with
x0,
x1,
x2.
Apply unknownprop_faa0906fd70676f18d9a02c8ff6587696be109a33d66d00ec0a508d4784f9592 with
aae7a.. x0 x1,
x2.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply unknownprop_0b996f3ce0151f58af219429b661039e0f6628ef50f5457c6338b0fd3feaa164 with
aae7a.. x0 x1,
x2.
Apply unknownprop_b4a3840982f4171d50a8011f1d1ddb72ad2a6c5880e9b141f24bf23602367bb7 with
x0,
x1,
x2.
The subproof is completed by applying H0.