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