Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Let x2 of type ι be given.
Apply unknownprop_ced40c82bec9d84d6ad8baec4b6c3b8f494372339c236cd16f6538e936263b63 with
λ x3 x4 : ι → (ι → ο) → ι . In ((λ x5 . SetAdjoin x5 (Sing 1)) x2) (x4 x0 x1).
Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with
Sep x0 (λ x3 . x1 x3),
ReplSep x0 (λ x3 . not (x1 x3)) (λ x3 . (λ x4 . SetAdjoin x4 (Sing 1)) x3),
(λ x3 . SetAdjoin x3 (Sing 1)) x2.
Apply unknownprop_8d2d2cad5b49b3f5b663b34a4b05b87bd91c0d0340dcf2eab94b6803f88f2fd8 with
x0,
λ x3 . not (x1 x3),
λ x3 . (λ x4 . SetAdjoin x4 (Sing 1)) x3,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.