-theorem all_append: ∀A,P,l2,l1. all A P l1 → all A P l2 → all A P (l1 @ l2).
+lemma all_hd: ∀A:Type[0]. ∀P:A→Prop. ∀a. P a → ∀l. all … P l → P (hd … l a).
+#A #P #a #Ha #l elim l -l [ #_ @Ha | #b #l #_ #Hl elim Hl // ]
+qed.
+
+lemma all_tl: ∀A:Type[0]. ∀P:A→Prop. ∀l. all … P l → all … P (tail … l).
+#A #P #l elim l -l // #b #l #IH #Hl elim Hl //
+qed.
+
+lemma all_nth: ∀A:Type[0]. ∀P:A→Prop. ∀a. P a → ∀i,l. all … P l → P (nth i … l a).
+#A #P #a #Ha #i elim i -i [ @all_hd // | #i #IH #l #Hl @IH /2/ ]
+qed.
+
+lemma all_append: ∀A,P,l2,l1. all A P l1 → all A P l2 → all A P (l1 @ l2).