#h #p #G #L #W #T #HW #HT #X #H
elim (cpm_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
<(HW … HW0) -W0 <(HT … HT0) -T0 //
qed.
lemma cnr_abbr_neg (h) (G) (L):
#h #p #G #L #W #T #HW #HT #X #H
elim (cpm_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
<(HW … HW0) -W0 <(HT … HT0) -T0 //
qed.
lemma cnr_abbr_neg (h) (G) (L):