Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_a5b0141dc7f70dc45c7d1f61b8342a4e97134fda6aab3192ae08a7f3d8c44b7c with
λ x2 x3 : ι → ι . In ((λ x4 . SetAdjoin x4 (Sing 1)) x1) (x3 x0).
Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with
x0,
Repl x0 (λ x2 . (λ x3 . SetAdjoin x3 (Sing 1)) x2),
(λ x2 . SetAdjoin x2 (Sing 1)) x1.
Apply unknownprop_63c308b92260dbfca8c9530846e6836ba3e6be221cc8e80fd61db913e01bdacf with
x0,
λ x2 . (λ x3 . SetAdjoin x3 (Sing 1)) x2,
x1.
The subproof is completed by applying H0.