(* Advanced inversion lemmas on reducibility ********************************)
(* Note: this property is unusual *)
(* Advanced inversion lemmas on reducibility ********************************)
(* Note: this property is unusual *)
-lemma cnx_inv_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⊥.
-#h #g #G #L #T #H elim H -L -T
-[ #L #k #d #Hkd #H
+lemma cnx_inv_crx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ➡[h, o] 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → ⊥.
+#h #o #G #L #T #H elim H -L -T
+[ #L #s #d #Hkd #H