Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_ca18603a3bd7d3baee9f63f87aac7064ee948e21e70ee2e74fd135602574a894 with
In x0 x1,
x0 = x1,
In x1 x0.
Apply unknownprop_f40b16152ee3fc8d75aedf90b5af38eeef30d8f4d82097ec4dc52d1487fa0c77 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.