+
+(* Basic inversions *********************************************************)
+
+lemma prelift_label_inv_d_sn (f) (l) (k1):
+ (𝗱k1) = ↑[f]l →
+ ∃∃k2. k1 = f@⧣❨k2❩ & 𝗱k2 = l.
+#f * [ #k ] #k1
+[ <prelift_label_d
+| <prelift_label_m
+| <prelift_label_L
+| <prelift_label_A
+| <prelift_label_S
+] #H0 destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma prelift_label_inv_m_sn (f) (l):
+ (𝗺) = ↑[f]l → 𝗺 = l.
+#f * [ #k ]
+[ <prelift_label_d
+| <prelift_label_m
+| <prelift_label_L
+| <prelift_label_A
+| <prelift_label_S
+] #H0 destruct //
+qed-.
+
+lemma prelift_label_inv_L_sn (f) (l):
+ (𝗟) = ↑[f]l → 𝗟 = l.
+#f * [ #k ]
+[ <prelift_label_d
+| <prelift_label_m
+| <prelift_label_L
+| <prelift_label_A
+| <prelift_label_S
+] #H0 destruct //
+qed-.
+
+lemma prelift_label_inv_A_sn (f) (l):
+ (𝗔) = ↑[f]l → 𝗔 = l.
+#f * [ #k ]
+[ <prelift_label_d
+| <prelift_label_m
+| <prelift_label_L
+| <prelift_label_A
+| <prelift_label_S
+] #H0 destruct //
+qed-.
+
+lemma prelift_label_inv_S_sn (f) (l):
+ (𝗦) = ↑[f]l → 𝗦 = l.
+#f * [ #k ]
+[ <prelift_label_d
+| <prelift_label_m
+| <prelift_label_L
+| <prelift_label_A
+| <prelift_label_S
+] #H0 destruct //
+qed-.
+
+(* Main inversions **********************************************************)
+
+theorem prelift_label_inj (f) (l1) (l2):
+ ↑[f]l1 = ↑[f]l2 → l1 = l2.
+#f * [ #k1 ] #l2 #Hl
+[ elim (prelift_label_inv_d_sn … Hl) -Hl #k2 #Hk #H0 destruct
+ >(tr_pap_inj ???? Hk) -Hk //
+| <(prelift_label_inv_m_sn … Hl) -l2 //
+| <(prelift_label_inv_L_sn … Hl) -l2 //
+| <(prelift_label_inv_A_sn … Hl) -l2 //
+| <(prelift_label_inv_S_sn … Hl) -l2 //
+]
+qed-.