Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Let x2 of type ι → ο be given.
Assume H0:
∀ x3 . In x3 x0 ⟶ x1 x3 ⟶ x2 x3.
Let x3 of type ι be given.
Apply unknownprop_ced40c82bec9d84d6ad8baec4b6c3b8f494372339c236cd16f6538e936263b63 with
λ x4 x5 : ι → (ι → ο) → ι . In x3 (x5 x0 x1) ⟶ x2 x3.
Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with
Sep x0 (λ x4 . x1 x4),
ReplSep x0 (λ x4 . not (x1 x4)) (λ x4 . (λ x5 . SetAdjoin x5 (Sing 1)) x4),
x3,
x2 x3 leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H3:
In x3 (Sep x0 (λ x4 . x1 x4)).
Apply unknownprop_6a6b356f855b99f3fbff4effcb62e3ee6aa23839e10650eb28a503a368c2bb09 with
x0,
x1,
x3,
x2 x3 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H0 with x3.
Apply unknownprop_021a576837934491f6aaf936d4c5a9c68d45f2b77fcd13cc395cfdeec72f7dac with
x0,
λ x4 . not (x1 x4),
λ x4 . (λ x5 . SetAdjoin x5 (Sing 1)) x4,
x3,
x2 x3 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x4 of type ι be given.
Apply H6 with
λ x5 x6 . x2 x6.
Apply H1 with
x4 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.