+lemma lifts_inv_atom1: ∀f,I,Y. ⬆*[f] ⓪{I} ≡ Y →
+ ∨∨ ∃∃s. I = Sort s & Y = ⋆s
+ | ∃∃i,j. @⦃i, f⦄ ≡ j & I = LRef i & Y = #j
+ | ∃∃l. I = GRef l & Y = §l.
+#f * #n #Y #H
+[ lapply (lifts_inv_sort1 … H)
+| elim (lifts_inv_lref1 … H)
+| lapply (lifts_inv_gref1 … H)
+] -H /3 width=5 by or3_intro0, or3_intro1, or3_intro2, ex3_2_intro, ex2_intro/
+qed-.
+
+lemma lifts_inv_atom2: ∀f,I,X. ⬆*[f] X ≡ ⓪{I} →
+ ∨∨ ∃∃s. X = ⋆s & I = Sort s
+ | ∃∃i,j. @⦃i, f⦄ ≡ j & X = #i & I = LRef j
+ | ∃∃l. X = §l & I = GRef l.
+#f * #n #X #H
+[ lapply (lifts_inv_sort2 … H)
+| elim (lifts_inv_lref2 … H)
+| lapply (lifts_inv_gref2 … H)
+] -H /3 width=5 by or3_intro0, or3_intro1, or3_intro2, ex3_2_intro, ex2_intro/
+qed-.
+