+lemma map_cons_inv_nil: ∀A,a,l1. map_cons A a l1 = ◊ → ◊ = l1.
+#A #a * // normalize #a1 #l1 #H destruct
+qed-.
+
+lemma map_cons_inv_cons: ∀A,a,a2,l2,l1. map_cons A a l1 = a2::l2 →
+ ∃∃a1,l. a::a1 = a2 & a:::l = l2 & a1::l = l1.
+#A #a #a2 #l2 * normalize
+[ #H destruct
+| #a1 #l1 #H destruct /2 width=5/
+]
+qed-.
+
+lemma map_cons_append: ∀A,a,l1,l2. map_cons A a (l1@l2) =
+ map_cons A a l1 @ map_cons A a l2.
+#A #a #l1 elim l1 -l1 // normalize /2 width=1/
+qed.
+