#h #I #G #L #K #i #HLK #n #X #H
elim (cpm_inv_lref1_drops ā¦ H) -H * [ // || #m ] #Y #V1 #V2 #HLY
lapply (drops_mono ā¦ HLK ā¦ HLY) -L #H destruct
#h #I #G #L #K #i #HLK #n #X #H
elim (cpm_inv_lref1_drops ā¦ H) -H * [ // || #m ] #Y #V1 #V2 #HLY
lapply (drops_mono ā¦ HLK ā¦ HLY) -L #H destruct