Some integrations from CerCo. In particular:

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

diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma
index 9af4b04a66d2ee4d882efdb99dc001a9d668de8d..f5bf4df9e43589533a511a307ff8281b3f10c1c0 100644 (file)
--- a/matita/matita/lib/basics/lists/listb.ma
+++ b/matita/matita/lib/basics/lists/listb.ma
@@ -105,7 +105,7 @@ let rec unique_append (S:DeqSet) (l1,l2: list S) on l1 ≝
   [ nil ⇒ l2
   | cons a tl ⇒ 
      let r ≝ unique_append S tl l2 in
-     if (memb S a r) then r else a::r
+     if memb S a r then r else a::r
   ].
 
 axiom unique_append_elim: ∀S:DeqSet.∀P: S → Prop.∀l1,l2.