Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x1,
x0.
Apply unknownprop_b8811722bb772bba243207d8ee471ba24f8b88e821f7737307414168e638d2c6 with
x0,
x1.
The subproof is completed by applying H0.