Let x0 of type ι → ο be given.
Let x1 of type ι → ο be given.
Let x2 of type ι be given.
Apply unknownprop_ca18603a3bd7d3baee9f63f87aac7064ee948e21e70ee2e74fd135602574a894 with
PNoLt_ x2 x0 x1,
PNoEq_ x2 x0 x1,
PNoLt_ x2 x1 x0.
Apply unknownprop_c5e1fd0612100f3930b78eccc1ac41f1cec2ebd1aa8641f1c54e36c3813ef296 with
x0,
x1,
x2.
The subproof is completed by applying H0.