commit by user andrea

[helm.git] / weblib / basics / list.ma

diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma
index 4e44ce298396d089a0fb97543c26cf94b770fa1e..d6c0661208c15e31c7b10684657a3f98bbd0060c 100644 (file)
--- a/weblib/basics/list.ma
+++ b/weblib/basics/list.ma
@@ -9,7 +9,7 @@
      \ /   GNU General Public License Version 2   
       V_______________________________________________________________ *)
 
-include "arithmetics/nat.ma".\ 5span class="error" title="disambiguation error"\ 6\ 5/span\ 6
+include "arithmetics/nat.ma".
 
 inductive list (A:Type[0]) : Type[0] :=
   | nil: list A
@@ -237,4 +237,4 @@ theorem fold_sum: ∀A,B. ∀I,J:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1
     \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈(I\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6J)} (f i).
 #A #B #I #J #nil #op #f (elim I) normalize 
   [>\ 5a href="cic:/matita/basics/list/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6 //|#a #tl #Hind <\ 5a href="cic:/matita/basics/list/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 //]
-qed.
\ No newline at end of file
+qed.