models ported

[helm.git] / helm / software / matita / contribs / didactic / algebra.ma

diff --git a/helm/software/matita/contribs/didactic/algebra.ma b/helm/software/matita/contribs/didactic/algebra.ma
index 3bfa6d7f7c02bef711e9c8c779a8f2b216b09e6f..17c30e341212c41882fc6d8c31ced3acf47251b0 100644 (file)
--- 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.