+(* Basic properties *********************************************************)
+
+lemma after_length: ∀cs1,cs2. ∥cs1∥ = |cs2| →
+ ∃∃cs. cs1 ⊚ cs2 ≡ cs & |cs| = |cs1| & ∥cs∥ = ∥cs2∥.
+#cs1 elim cs1 -cs1
+[ #cs2 #H >(length_inv_zero_sn … H) -cs2 /2 width=4 by after_empty, ex3_intro/
+| * #cs1 #IH #cs2 #Hcs
+ [ elim (length_inv_succ_sn … Hcs) -Hcs
+ #tl #b #Hcs #H destruct
+ ]
+ elim (IH … Hcs) -IH -Hcs
+ #cs #Hcs #H1 #H2 [ @(ex3_intro … (b@cs)) | @(ex3_intro … (Ⓕ@cs)) ] /2 width=1 by after_true, after_false, colength_cons/
+]
+qed-.
+