-lemma cnr_abst: ∀a,I,L,V,W,T. L ⊢ 𝐍⦃W⦄ → L. ⓑ{I} V ⊢ 𝐍⦃T⦄ → L ⊢ 𝐍⦃ⓛ{a}W.T⦄.
-#a #I #L #V #W #T #HW #HT #X #H
-elim (cpr_fwd_abst1 … H I V) -H #W0 #T0 #HW0 #HT0 #H destruct
+lemma cnr_abst: ∀a,L,W,T. L ⊢ 𝐍⦃W⦄ → L.ⓛW ⊢ 𝐍⦃T⦄ → L ⊢ 𝐍⦃ⓛ{a}W.T⦄.
+#a #L #W #T #HW #HT #X #H
+elim (cpr_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct