X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Ftutorial%2Fchapter6.ma;h=38fb54a0c3afa3a96be06c7d31a35285d3a651ff;hb=a09b60bd574adf1a7d3e423023009cb20c79d449;hp=fb38f2d316e8d9db3ec58a345f34ee2ae513dd5a;hpb=f66ae73597b06a5bf8b0ef82d5253bf0e5aba7fc;p=helm.git

diff --git a/matita/matita/lib/tutorial/chapter6.ma b/matita/matita/lib/tutorial/chapter6.ma
index fb38f2d31..38fb54a0c 100644
--- a/matita/matita/lib/tutorial/chapter6.ma
+++ b/matita/matita/lib/tutorial/chapter6.ma
@@ -343,6 +343,20 @@ let rec memb (S:DeqSet) (x:S) (l: list S) on l  ≝
   | cons a tl ⇒ (x == a) ∨ memb S x tl
   ].
   
+lemma memb_hd: ∀S,a,l. memb S a (a::l) = true.
+#S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) //
+qed.
+
+lemma memb_cons: ∀S,a,b,l. 
+  memb S a l = true → memb S a (b::l) = true.
+#S #a #b #l normalize cases (a==b) normalize // 
+qed.
+
+lemma memb_single: ∀S,a,x. memb S a [x] = true → a = x.
+#S #a #x normalize cases (true_or_false … (a==x)) #H
+  [#_ >(\P H) // |>H normalize #abs @False_ind /2/]
+qed.
+
 let rec uniqueb (S:DeqSet) l on l : bool ≝
   match l with 
   [ nil ⇒ true
@@ -405,7 +419,7 @@ lemma memb_map_to_exists: ∀A,B:DeqSet.∀f:A→B.∀l,b.
 #A #B #f #l elim l 
   [#b normalize #H destruct (H) 
   |#a #tl #Hind #b #H cases (orb_true_l … H) 
-    [#eqb @(ex_intro … a) <(\P eqb) % // normalize >(\b (refl ? a)) //
+    [#eqb @(ex_intro … a) <(\P eqb) % // 
     |#memb cases (Hind … memb) #a * #mema #eqb
      @(ex_intro … a) /3/
     ]