Let x0 of type ο be given.
Let x1 of type ο be given.
Apply unknownprop_896ccc9f209efa8a895211d65adb5a90348b419f100f6ab5e9762ce4d7fa9cc1 with
x0 ⟶ x1,
x1 ⟶ x0.
Apply unknownprop_a8d0a23b866eb3c6586d6230553d1bf85bfc05d878ba9cde7043ac2ed660e0cb with
x0,
x1.
The subproof is completed by applying H0.