| #f1 #I1 #L1 #V1 #Hf1 #IH #I2 #L2 #V2 *
[ -IH #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 //
#H destruct #g1 #Hgf1 >(injective_next … Hgf1) -g1
| #f1 #I1 #L1 #V1 #Hf1 #IH #I2 #L2 #V2 *
[ -IH #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 //
#H destruct #g1 #Hgf1 >(injective_next … Hgf1) -g1