Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ο be given.
Assume H0:
PNoEq_ x0 (λ x4 . In x4 x1) (λ x4 . In x4 x2) ⟶ x3.
Apply H0.
Apply unknownprop_b7c7a090ca47d83894301167c54772cc587bbb21de668c0b72273825ec0064b9 with
x0,
x1,
x2.
The subproof is completed by applying H1.