Let x0 of type ι be given.
Apply H0 with
λ x1 x2 . nIn x0 x1.
The subproof is completed by applying unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with x0.
Apply L1.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with x0.