X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdidactic%2Falgebra.ma;h=17c30e341212c41882fc6d8c31ced3acf47251b0;hb=bb7af347df386afcd3ea2adea8e7e982e3a5a253;hp=3bfa6d7f7c02bef711e9c8c779a8f2b216b09e6f;hpb=38916383ce5964d801930f252e7942f90062530e;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.