From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Wed, 7 Mar 2012 10:37:05 +0000 (+0000)
Subject: commit by user utente2
X-Git-Tag: make_still_working~1883
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=111e641bb0772a542293b796c9d4a18fc9d58a00;p=helm.git

commit by user utente2
---

diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma
index 39fdb1bd5..4e44ce298 100644
--- a/weblib/basics/list.ma
+++ b/weblib/basics/list.ma
@@ -134,7 +134,7 @@ let rec rev_append S (l1,l2:a href="cic:/matita/basics/list/list.ind(1,0,1)"li
 
 definition reverse ≝λS.λl.a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"rev_append/a S l a title="nil" href="cic:/fakeuri.def(1)"[/a].
 
-lemma reverse_single : ∀S,a. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S a title="cons" href="cic:/fakeuri.def(1)"[/aa] a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="cons" href="cic:/fakeuri.def(1)"[/aa]. 
+lemma reverse_single : ∀S,a. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]). 
 // qed.
 
 lemma rev_append_def : ∀S,l1,l2. 
@@ -142,7 +142,7 @@ lemma rev_append_def : ∀S,l1,l2.
 #S #l1 elim l1 normalize // 
 qed.
 
-lemma reverse_cons : ∀S,a,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l)a title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aa].
+lemma reverse_cons : ∀S,a,l. a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S (aa title="cons" href="cic:/fakeuri.def(1)":/a:l) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l)a title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]).
 #S #a #l whd in ⊢ (??%?); // 
 qed.
 
@@ -158,7 +158,7 @@ normalize // qed.
 (* an elimination principle for lists working on the tail;
 useful for strings *)
 lemma list_elim_left: ∀S.∀P:a href="cic:/matita/basics/list/list.ind(1,0,1)"list/a S → Prop. P (a href="cic:/matita/basics/list/list.con(0,1,1)"nil/a S) →
-(∀a.∀tl.P tl → P (tla title="append" href="cic:/fakeuri.def(1)"@/aa title="cons" href="cic:/fakeuri.def(1)"[/aa])) → ∀l. P l.
+(∀a.∀tl.P tl → P (tla title="append" href="cic:/fakeuri.def(1)"@/a(aa title="cons" href="cic:/fakeuri.def(1)":/a:a title="nil" href="cic:/fakeuri.def(1)"[/a]))) → ∀l. P l.span class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"/span
 #S #P #Pnil #Pstep #l <(a href="cic:/matita/basics/list/reverse_reverse.def(9)"reverse_reverse/a … l) 
 generalize in match (a href="cic:/matita/basics/list/reverse.def(2)"reverse/a S l); #l elim l //
 #a #tl #H >a href="cic:/matita/basics/list/reverse_cons.def(7)"reverse_cons/a @Pstep //