Still bugged.

[helm.git] / matita / library / decidable_kit / fintype.ma

diff --git a/matita/library/decidable_kit/fintype.ma b/matita/library/decidable_kit/fintype.ma
index ffd41d20615274559209b572b81d29a9d0884e22..8f5de6e0aa85f5d9e445c2b86ed2b7705a4adba3 100644 (file)
--- a/matita/library/decidable_kit/fintype.ma
+++ b/matita/library/decidable_kit/fintype.ma
@@ -46,7 +46,7 @@ rewrite < (leb_eqb x n); rewrite > H1; reflexivity;
 qed.
 
 lemma mem_filter :
-  ∀d1,d2:eqType.(*∀y:d1.*)∀x:d2.∀l:list d1.∀p:d1 → option d2.
+  ∀d1,d2:eqType.∀x:d2.∀l:list d1.∀p:d1 → option d2.
   (∀y.mem d1 y l = true → 
     match (p y) with [None ⇒ false | (Some q) ⇒ cmp d2 x q] = false) →
   mem d2 x (filter d1 d2 p l) = false.