Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply andE with
In x2 x0,
nIn x2 x1.
Apply unknownprop_fc31fd753a6508f51d92a8c5bd413707035a5f3c142d3e7d222d5f25ed6c3a34 with
x0,
x1,
x2.
The subproof is completed by applying H0.