- some additions and renaming ...

[helm.git] / matita / matita / lib / basics / lists / list.ma

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index a34ac3c9cd1c7e9026adf18600f312dd38b75740..a51998ae420e4a66108a74e59206545b413c5f09 100644 (file)
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -445,12 +445,18 @@ lemma All_nth : ∀A,P,n,l.
   ]
 ] qed.
 
+(**************************** Allr ******************************)
+
 let rec Allr (A:Type[0]) (R:relation A) (l:list A) on l : Prop ≝
 match l with
 [ nil       ⇒ True
 | cons a1 l ⇒ match l with [ nil ⇒ True | cons a2 _ ⇒ R a1 a2 ∧ Allr A R l ]
 ].
 
+lemma Allr_fwd_append_sn: ∀A,R,l1,l2. Allr A R (l1@l2) → Allr A R l1.
+#A #R #l1 elim l1 -l1 // #a1 * // #a2 #l1 #IHl1 #l2 * /3 width=2/
+qed-.
+
 (**************************** Exists *******************************)
 
 let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝