Let x0 of type ι be given.
Let x1 of type ι be given.
Apply prop_ext_2 with
Subq x0 x1,
0ac37.. x0 x1 = x1 leaving 2 subgoals.
Apply set_ext with
0ac37.. x0 x1,
x1 leaving 2 subgoals.
Apply unknownprop_c16c0737d29e3b3e820cf0e7f73a8868a90e8434c78c164566097cca1a566416 with
x0,
x1,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying Subq_ref with x1.
The subproof is completed by applying unknownprop_0fa3c716de2f83f3d57854877ac4d59bd5007991ec359a1e0159fb506bca2548 with x0, x1.
Apply H0 with
λ x2 x3 . Subq x0 x2.
The subproof is completed by applying unknownprop_888c4c61f9af73a08c8a3d54aaeed5dafb313e52bc146db81320dd33dcdade2c with x0, x1.