1) \ldots here and there

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / option_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma
index 4f362a873737f6a56c8fcd5acd97d9b8ee189002..9a81564fea2fb4b95869cdee43f6a4f1b70ccb69 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma
@@ -13,15 +13,11 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
-(*                           Progetto FreeScale                           *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
+(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
 (*                                                                        *)
-(* Questo materiale fa parte della tesi:                                  *)
-(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
-(*                                                                        *)
-(*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
 include "freescale/bool_lemmas.ma".
@@ -36,7 +32,7 @@ nlemma option_destruct_some_some : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1
  nchange with (match Some T x2 with [ None ⇒ False | Some a ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → False.
@@ -60,14 +56,14 @@ nlemma symmetric_eqoption :
  (symmetricT T bool f) →
  (eq_option T op1 op2 f = eq_option T op2 op1 f).
  #T; #op1; #op2; #f; #H;
- napply (option_ind T ??? op1);
- napply (option_ind T ??? op2);
+ nelim op1;
+ nelim op2;
  nnormalize;
- ##[ ##1: napply (refl_eq ??)
- ##| ##2,3: #H; napply (refl_eq ??)
+ ##[ ##1: napply refl_eq
+ ##| ##2,3: #H; napply refl_eq
  ##| ##4: #a; #a0;
           nrewrite > (H a0 a);
-          napply (refl_eq ??)
+          napply refl_eq
  ##]
 nqed.
 
@@ -76,16 +72,16 @@ nlemma eq_to_eqoption :
  (∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
  (op1 = op2 → eq_option T op1 op2 f = true).
  #T; #op1; #op2; #f; #H;
- napply (option_ind T ??? op1);
- napply (option_ind T ??? op2);
+ nelim op1;
+ nelim op2;
  nnormalize;
- ##[ ##1: #H1; napply (refl_eq ??)
+ ##[ ##1: #H1; napply refl_eq
  ##| ##2: #a; #H1; nelim (option_destruct_none_some ?? H1)
  ##| ##3: #a; #H1; nelim (option_destruct_some_none ?? H1)
  ##| ##4: #a; #a0; #H1;
-          nrewrite > (option_destruct_some_some ??? H1);
-          nrewrite > (H a a (refl_eq ??));
-          napply (refl_eq ??)
+          nrewrite > (option_destruct_some_some … H1);
+          nrewrite > (H a a (refl_eq …));
+          napply refl_eq
  ##]
 nqed.
 
@@ -94,13 +90,13 @@ nlemma eqoption_to_eq :
  (∀x1,x2:T.f x1 x2 = true → x1 = x2) →
  (eq_option T op1 op2 f = true → op1 = op2).
  #T; #op1; #op2; #f; #H;
- napply (option_ind T ??? op1);
- napply (option_ind T ??? op2);
+ nelim op1;
+ nelim op2;
  nnormalize;
- ##[ ##1: #H1; napply (refl_eq ??)
- ##| ##2,3: #a; #H1; napply (bool_destruct ??? H1)
+ ##[ ##1: #H1; napply refl_eq
+ ##| ##2,3: #a; #H1; napply (bool_destruct … H1)
  ##| ##4: #a; #a0; #H1;
-          nrewrite > (H ?? H1);
-          napply (refl_eq ??)
+          nrewrite > (H … H1);
+          napply refl_eq
  ##]
 nqed.