lemma cpt_inv_gref_sn (h) (n) (G) (L) (l):
∀X2. ⦃G,L⦄ ⊢ §l ⬆[h,n] X2 → ∧∧ X2 = §l & n = 0.
#h #n #G #L #l #X2 * #c #Hc #H elim (cpg_inv_gref1 … H) -H
lemma cpt_inv_gref_sn (h) (n) (G) (L) (l):
∀X2. ⦃G,L⦄ ⊢ §l ⬆[h,n] X2 → ∧∧ X2 = §l & n = 0.
#h #n #G #L #l #X2 * #c #Hc #H elim (cpg_inv_gref1 … H) -H