A few integrations (closed an axiom in finset).

[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 a4ba4cce1ee217651b21a3779204aa3637185af0..1eaab72bab2d3cfa64636c0784aa3dc1f5c3303c 100644 (file)
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -119,6 +119,7 @@ lemma compare_append : ∀A,l1,l2,l3,l4. l1@l2 = l3@l4 →
     ]
   ]
 qed.
+
 (**************************** iterators ******************************)
 
 let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝