From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 20 Oct 2008 14:06:53 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4652
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a773ee47c7539bdbafbfdca306424abaee4a9024;p=helm.git

...
---

diff --git a/helm/software/matita/contribs/didactic/algebra.ma b/helm/software/matita/contribs/didactic/algebra.ma
index 3bfa6d7f7..17c30e341 100644
--- a/helm/software/matita/contribs/didactic/algebra.ma
+++ b/helm/software/matita/contribs/didactic/algebra.ma
@@ -89,23 +89,13 @@ case EPlus.
   by H1 we proved (∀v.val (subst e1 E1 i) v = val (subst e1 E2 i) v) (H11).  
   by H2 we proved (∀v.val (subst e2 E1 i) v = val (subst e2 E2 i) v) (H22).
   the thesis becomes 
-    (∀v. val (EPlus (subst e1 E1 i) (subst e2 E1 i)) v =
-         val (EPlus (subst e1 E2 i) (subst e2 E2 i)) v).
+    (∀v. val (subst e1 E1 i) v + val (subst e2 E1 i) v =
+         val (subst e1 E2 i) v + val (subst e2 E2 i) v).
   assume v : (ℕ → ℕ).       
-  conclude (val (EPlus (subst e1 E1 i) (subst e2 E1 i)) v)
-         = (val (EPlus (subst e1 E1 i) (subst e2 E2 i)) v).
-    = (val (EPlus (subst e1 E2 i) (subst e2 E2 i)) v) by H22.
-  assume n : ℕ.
-  the thesis becomes 
-    (equiv 
-      (if (eqb i n) then E1 else (X n))
-      (subst (X n) E2 i)).
-  the thesis becomes 
-    (equiv 
-      (if (eqb i n) then E1 else (X n))
-      (if (eqb i n) then E2 else (X n))).
-  we proceed by cases ...    
-  
-
-
-  
\ No newline at end of file
+  conclude 
+    (val (subst e1 E1 i) v + val (subst e2 E1 i) v) =
+    (val (subst e1 E1 i) v + val (subst e2 E2 i) v) by H11.
+  conclude 
+    (val (subst e1 E1 i) v + val (subst e2 E1 i) v) =
+    (val (subst e1 E1 i) v + val (subst e2 E1 i) v) by H22.
+  done.