#R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL
elim (lexs_sdj_split … ceq_ext … HL 𝐈𝐝 ?) -HL
[ #L0 #HL10 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] -H1R
#R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL
elim (lexs_sdj_split … ceq_ext … HL 𝐈𝐝 ?) -HL
[ #L0 #HL10 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] -H1R