From 5fbe7da7019bda8fead167c8b1da1b06625551b3 Mon Sep 17 00:00:00 2001
From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Wed, 9 Nov 2011 10:13:47 +0000
Subject: [PATCH] commit by user andrea

---
 weblib/tutorial/chapter4.ma | 39 +++++++++++++------------------------
 1 file changed, 13 insertions(+), 26 deletions(-)

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 77e42066e..00b70a0da 100644
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -172,31 +172,18 @@ interpretation "in_prl" 'in_l E = (in_prl ? E).
 
 lemma not_epsilon_lp :∀S.∀pi:a href="cic:/matita/tutorial/chapter4/pitem.ind(1,0,1)"pitem/a S. a title="logical not" href="cic:/fakeuri.def(1)"¬/a ((a title="in_pl" href="cic:/fakeuri.def(1)"ℓ/a pi) a title="nil" href="cic:/fakeuri.def(1)"[/a]).
 #S #pi (elim pi) normalize /2/
-  [#pi1 #pi2 #H1 #H2 % * /2/ * #w1 * #w2 * * /2/;
-
-lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = [ ] → w1 = [ ].
-#S w1; nelim w1; //. #x tl IH w2; nnormalize; #abs; ndestruct; nqed.
-
-(* lemma 12 *)
-nlemma epsilon_in_true : ∀S.∀e:pre S. [ ] ∈ e ↔ \snd e = true.
-#S r; ncases r; #e b; @; ##[##2: #H; nrewrite > H; @2; /2/; ##] ncases b;//; 
-nnormalize; *; ##[##2:*] nelim e;
-##[ ##1,2: *; ##| #c; *; ##| #c; nnormalize; #; ndestruct; ##| ##7: #p H;
-##| #r1 r2 H G; *; ##[##2: /3/ by or_intror]
-##| #r1 r2 H1 H2; *; /3/ by or_intror, or_introl; ##]
-*; #w1; *; #w2; *; *; #defw1; nrewrite > (append_eq_nil … w1 w2 …); /3/ by {};//;
-nqed.
-
-nlemma not_epsilon_lp : ∀S:Alpha.∀e:pitem S. ¬ ((𝐋\p e) [ ]).
-#S e; nelim e; nnormalize; /2/ by nmk;
-##[ #; @; #; ndestruct;
-##| #r1 r2 n1 n2; @; *; /2/; *; #w1; *; #w2; *; *; #H;
-    nrewrite > (append_eq_nil …H…); /2/;
-##| #r1 r2 n1 n2; @; *; /2/;
-##| #r n; @; *; #w1; *; #w2; *; *; #H;     
-    nrewrite > (append_eq_nil …H…); /2/;##]
-nqed.
-
-ndefinition lo ≝ λS:Alpha.λ
+  [#pi1 #pi2 #H1 #H2 % * /2/ * #w1 * #w2 * * #appnil 
+   cases (a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"nil_to_nil/a … appnil) /2/
+  |#p11 #p12 #H1 #H2 % * /2/
+  |#pi #H % * #w1 * #w2 * * #appnil (cases (a href="cic:/matita/tutorial/chapter3/nil_to_nil.def(5)"nil_to_nil/a … appnil)) /2/
+  ]
+qed.
+
+lemma if_true_epsilon: ∀S.∀e:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S. a title="snd" href="cic:/fakeuri.def(1)"\snd/a e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → ((a title="in_prl" href="cic:/fakeuri.def(1)"ℓ/a e) a title="nil" href="cic:/fakeuri.def(1)"[/a]).
+#S #e #H %2 >H // qed.
+
+lemma if_epsilon_true : ∀S.∀e:a href="cic:/matita/tutorial/chapter4/pre.def(1)"pre/a S. a title="nil" href="cic:/fakeuri.def(1)"[/a ] a title="in_prl mem" href="cic:/fakeuri.def(1)"∈/a e → a title="snd" href="cic:/fakeuri.def(1)"\snd/a e a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+#S * #pi #b * [#abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /2/] cases b normalize // @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a
+qed.
 
 
-- 
2.39.2