Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_e75b5686f39ea4dca8e72e616b0514162494e9e895f52dbe14fa1984a713fe57 with
e5b72.. (472ec.. x0),
λ x2 . ∃ x3 . and (prim1 x3 x0) (1beb9.. x3 x2),
x1.
The subproof is completed by applying H1.