lemma cix_lref: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃#i⦄.
#h #g #G #L #i #HL #H elim (crx_inv_lref … H) -h #I #K #V #HLK
lemma cix_lref: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃#i⦄.
#h #g #G #L #i #HL #H elim (crx_inv_lref … H) -h #I #K #V #HLK