commit by user utente2

diff --git a/weblib/basics/list.ma b/weblib/basics/list.ma
index 39fdb1bd5ca9f550d6f3b1d37e72395af2c8546d..4e44ce298396d089a0fb97543c26cf94b770fa1e 100644 (file)
--- a/weblib/basics/list.ma
+++ b/weblib/basics/list.ma
@@ -134,7 +134,7 @@ let rec rev_append S (l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6li
 
 definition reverse ≝λS.λl.\ 5a href="cic:/matita/basics/list/rev_append.fix(0,1,1)"\ 6rev_append\ 5/a\ 6 S l \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
 
-lemma reverse_single : ∀S,a. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a] \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a]. 
+lemma reverse_single : ∀S,a. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]). 
 // 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. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a].
+lemma reverse_cons : ∀S,a,l. \ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l)\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]).
 #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:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 S → Prop. P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 S) →
-(∀a.∀tl.P tl → P (tl\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a])) → ∀l. P l.
+(∀a.∀tl.P tl → P (tl\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]))) → ∀l. P l.\ 5span class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"\ 6\ 5/span\ 6
 #S #P #Pnil #Pstep #l <(\ 5a href="cic:/matita/basics/list/reverse_reverse.def(9)"\ 6reverse_reverse\ 5/a\ 6 … l) 
 generalize in match (\ 5a href="cic:/matita/basics/list/reverse.def(2)"\ 6reverse\ 5/a\ 6 S l); #l elim l //
 #a #tl #H >\ 5a href="cic:/matita/basics/list/reverse_cons.def(7)"\ 6reverse_cons\ 5/a\ 6 @Pstep //