X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Foct_lemmas.ma;h=d6c0145980c93c28c7635ff3c592d61d828a3e6f;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=3a29cc1b75360949c51fced2ea550e09cf6d2472;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma
index 3a29cc1b7..d6c014598 100755
--- a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Sviluppo: 2008-2010                                                  *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -27,7 +27,6 @@ include "num/bool_lemmas.ma".
 (* OTTALI *)
 (* ****** *)
 
-(*
 ndefinition oct_destruct_aux ≝
 Πn1,n2:oct.ΠP:Prop.n1 = n2 →
  match eq_oct n1 n2 with [ true ⇒ P → P | false ⇒ P ].
@@ -39,7 +38,6 @@ ndefinition oct_destruct : oct_destruct_aux.
  nnormalize;
  napply (λx.x).
 nqed.
-*)
 
 nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
  #n1; #n2; #H;
@@ -63,7 +61,7 @@ nlemma eqoct_to_eq : ∀n1,n2.eq_oct n1 n2 = true → n1 = n2.
  ncases n2;
  nnormalize;
  ##[ ##1,10,19,28,37,46,55,64: #H; napply refl_eq
- ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.