Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ο be given.
Assume H1:
∀ x3 . In x3 x0 ⟶ x2 (Inj1 x3).
Apply unknownprop_4e401b8b934d31731f655157d6e702ad6580dcf49964fd29729f5ecb3d39e139 with
x0,
x1,
x2 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H2:
(λ x4 . and (In x4 x0) (x1 = Inj1 x4)) x3.
Apply andE with
In x3 x0,
x1 = Inj1 x3,
x2 x1 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply H4 with
λ x4 x5 . x2 x5.
Apply H1 with
x3.
The subproof is completed by applying H3.