X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flists%2Flist.ma;h=a51998ae420e4a66108a74e59206545b413c5f09;hb=81fc94f4f091ec35d41e2711207218d255b75273;hp=a34ac3c9cd1c7e9026adf18600f312dd38b75740;hpb=39aab7babf51252cecb81a66af82fe797e8dcbe7;p=helm.git

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index a34ac3c9c..a51998ae4 100644
--- 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 ≝