-lemma cpce_inv_ldef_sn (h) (G) (K) (X2):
- ∀V. ⦃G,K.ⓓV⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2.
-#h #G #Y #X2 #X
-@(insert_eq_0 … (Y.ⓓX)) #Y1
+lemma cpce_inv_atom_sn (h) (G) (i):
+ ∀X2. ⦃G,⋆⦄ ⊢ #i ⬌η[h] X2 → #i = X2.
+#h #G #i0 #X2
+@(insert_eq_0 … LAtom) #Y
+@(insert_eq_0 … (#i0)) #X1
+* -G -Y -X1 -X2
+[ #G #L #s #_ #_ //
+| #G #i #_ #_ //
+| #I #G #K #_ #_ //
+| #G #K #V #_ #_ //
+| #G #K #W #_ #_ #_ //
+| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #_ #H destruct
+| #I #G #K #T #U #i #_ #_ #_ #H destruct
+| #G #L #l #_ #_ //
+| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
+]
+qed-.
+
+lemma cpce_inv_unit_sn (h) (I) (G) (K):
+ ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2.
+#h #I0 #G #K0 #X2
+@(insert_eq_0 … (K0.ⓤ{I0})) #Y
+@(insert_eq_0 … (#0)) #X1
+* -G -Y -X1 -X2
+[ #G #L #s #_ #_ //
+| #G #i #_ #_ //
+| #I #G #K #_ #_ //
+| #G #K #V #_ #_ //
+| #G #K #W #_ #_ #_ //
+| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #_ #H destruct
+| #I #G #K #T #U #i #_ #_ #H #_ destruct
+| #G #L #l #_ #_ //
+| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
+]
+qed-.
+
+lemma cpce_inv_ldef_sn (h) (G) (K) (V):
+ ∀X2. ⦃G,K.ⓓV⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2.
+#h #G #K0 #V0 #X2
+@(insert_eq_0 … (K0.ⓓV0)) #Y