Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_3848cfb1fd522cb609408da39f227a9c05924a24919f21041d0880590b824ef5 with
λ x2 . In x1 x2,
λ x2 . In x2 x0.
Apply unknownprop_8cedd81d70e25b63b7556c6282ff8cb3f8cd5d78cfe400c053c245452b171ad5 with
x0,
x1.
The subproof is completed by applying H0.