...

diff --git a/helm/software/matita/contribs/didactic/algebra.ma b/helm/software/matita/contribs/didactic/algebra.ma
index eabbdb1104838f83fb1754e870b136dd2f381b85..3bfa6d7f7c02bef711e9c8c779a8f2b216b09e6f 100644 (file)
--- a/helm/software/matita/contribs/didactic/algebra.ma
+++ b/helm/software/matita/contribs/didactic/algebra.ma
@@ -8,11 +8,11 @@ notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp
 interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else _ e t f).
 
 inductive F : Type ≝
-| X       : ℕ → F
-| EPlus   : F → F → F
-| ETimes  : F → F → F
 | EZero   : F
 | EOne    : F
+| EPlus   : F → F → F
+| ETimes  : F → F → F
+| X       : ℕ → F
 .
 
 let rec val (E : F) (v : ℕ → ℕ) on E : ℕ :=
@@ -67,7 +67,34 @@ assume i : ℕ.
 suppose (equiv E1 E2) (H).
 we proceed by induction on G to prove
   (equiv (subst G E1 i) (subst G E2 i)).
-case X.
+case EZero.
+  the thesis becomes (equiv (subst EZero E1 i) (subst EZero E2 i)).
+  the thesis becomes (equiv EZero (subst EZero E2 i)).
+  the thesis becomes (equiv EZero EZero).
+  the thesis becomes (∀v.val EZero v = val EZero v).
+  assume v : (ℕ → ℕ).
+  the thesis becomes (0 = val EZero v).
+  the thesis becomes (0 = 0).
+  done.
+case EOne.  
+  the thesis becomes (∀v.val EOne v = val EOne v).
+  assume v : (ℕ → ℕ).
+  the thesis becomes (1 = 1).
+  done.
+case EPlus.
+  assume e1 : F.
+  by induction hypothesis we know (equiv (subst e1 E1 i) (subst e1 E2 i)) (H1).
+  assume e2 : F.
+  by induction hypothesis we know (equiv (subst e2 E1 i) (subst e2 E2 i)) (H2).
+  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).
+  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