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