| #c #G #L1 #V1 #V2 #W2 #_ #HVW2 #IH #X #H
elim (lsubr_inv_abst2 … H) -H * #L2 [2: #V ] #HL21 #H destruct
/4 width=3 by cpg_delta, cpg_ell, cpg_ee/
| #c #G #L1 #V1 #V2 #W2 #_ #HVW2 #IH #X #H
elim (lsubr_inv_abst2 … H) -H * #L2 [2: #V ] #HL21 #H destruct
/4 width=3 by cpg_delta, cpg_ell, cpg_ee/