Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Apply unknownprop_d4c6f9663742385071dd283da85a9397dc2dfd0eede50c9fd289b7b23ca97cdd with
In x2 (Repl x0 (λ x3 . x1 x3)),
∃ x3 . and (In x3 x0) (x2 = x1 x3).
The subproof is completed by applying unknownprop_422bc2d8d5c5891fd637c087651fa7529b2c1da4bb1da1788f9bfacb9979ef9e with x0, x1, x2.