Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_7f3377c88b4409d85225bd10726cc6caca85db3671a8e3d8d0e75f9aea9723e4 with
x0,
x1.
Apply unknownprop_17394c01713608728cb81e433416d32f861c0ef29d5be8c5e8c1bd2291cd9c8d with
SNoLev x0,
SNoLev x1,
λ x2 . In x2 x0,
λ x2 . In x2 x1.
Apply unknownprop_e25a9320de659de01aa92cbaed9321cd49a58ef5c32367fe25748c540abd071a with
x0,
x1.
The subproof is completed by applying H0.