>(deg_mono … Hkl2 … Hkl1) -h -k -l2 //
| #G #L #K #V #i #l1 #HLK #_ #IHV #l2 #H
elim (da_inv_lref … H) -H * #K0 #V0 [| #l0 ] #HLK0 #HV0 [| #Hl0 ]
- lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct /2 width=1/
+ lapply (drop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct /2 width=1/
| #G #L #K #W #i #l1 #HLK #_ #IHW #l2 #H
elim (da_inv_lref … H) -H * #K0 #W0 [| #l0 ] #HLK0 #HW0 [| #Hl0 ]
- lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct /3 width=1/
+ lapply (drop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct /3 width=1/
| #a #I #G #L #V #T #l1 #_ #IHT #l2 #H
lapply (da_inv_bind … H) -H /2 width=1/
| #I #G #L #V #T #l1 #_ #IHT #l2 #H