Let x0 of type ο be given.
Let x1 of type ο be given.
Assume H0: x0 = x1.
Apply unknownprop_338c7acdd03d67524265461947221f0d28eab398796d7d45302790abbbe8b64d with
x0,
x1.
Apply unknownprop_4495ba5f0974dc3872c3c4ed71ccc207b101483f9fc5bafe9bb0cc1f775d85b8 with
x0,
x1.
The subproof is completed by applying H0.