Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_e27cc1084b79022284e382e1b6bc2015115f79977a5cda617e7753aa1838b538 with
λ x2 x3 : ι → ι → ο . x3 x0 x1.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
Subq x1 (SNoElts_ x0),
∀ x2 . In x2 x0 ⟶ exactly1of2 (In ((λ x3 . SetAdjoin x3 (Sing 1)) x2) x1) (In x2 x1) leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.