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