+lemma cpm_inv_lref1_ctop (n) (h) (G):
+ ∀X2,i. ⦃G,⋆⦄ ⊢ #i ➡[n,h] X2 → ∧∧ X2 = #i & n = 0.
+#n #h #G #X2 * [| #i ] #H
+[ elim (cpm_inv_zero1 … H) -H *
+ [ #H1 #H2 destruct /2 width=1 by conj/
+ | #Y #X1 #X2 #_ #_ #H destruct
+ | #m #Y #X1 #X2 #_ #_ #H destruct
+ ]
+| elim (cpm_inv_lref1 … H) -H *
+ [ #H1 #H2 destruct /2 width=1 by conj/
+ | #Z #Y #X0 #_ #_ #H destruct
+ ]
+]
+qed.
+