X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fcommon%2Foption_lemmas.ma;h=1d25b4bd95bfed16bf577492e00721d60aab517f;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=7e73870bf5d5fa54061829e32f5a95cce5ba9236;hpb=b886a562ccbfc3f63b8f64a135bcf70e4b189999;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma
index 7e73870bf..1d25b4bd9 100644
--- a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma
@@ -54,12 +54,12 @@ nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False.
 nqed.
 
 nlemma symmetric_eqoption :
-∀T:Type.∀f:T → T → bool.∀op1,op2:option T.
+∀T:Type.∀f:T → T → bool.
  (symmetricT T bool f) →
- (eq_option T f op1 op2 = eq_option T f op2 op1).
- #T; #f; #op1; #op2; #H;
- nelim op1;
- nelim op2;
+ (∀op1,op2:option T.
+  (eq_option T f op1 op2 = eq_option T f op2 op1)).
+ #T; #f; #H;
+ #op1; #op2; nelim op1; nelim op2;
  nnormalize;
  ##[ ##1: napply refl_eq
  ##| ##2,3: #H; napply refl_eq
@@ -70,12 +70,12 @@ nlemma symmetric_eqoption :
 nqed.
 
 nlemma eq_to_eqoption :
-∀T.∀f:T → T → bool.∀op1,op2:option T.
+∀T.∀f:T → T → bool.
  (∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
- (op1 = op2 → eq_option T f op1 op2 = true).
- #T; #f; #op1; #op2; #H;
- nelim op1;
- nelim op2;
+ (∀op1,op2:option T.
+  (op1 = op2 → eq_option T f op1 op2 = true)).
+ #T; #f; #H;
+ #op1; #op2; nelim op1; nelim op2;
  nnormalize;
  ##[ ##1: #H1; napply refl_eq
  ##| ##2: #a; #H1;
@@ -91,12 +91,12 @@ nlemma eq_to_eqoption :
 nqed.
 
 nlemma eqoption_to_eq :
-∀T.∀f:T → T → bool.∀op1,op2:option T.
+∀T.∀f:T → T → bool.
  (∀x1,x2:T.f x1 x2 = true → x1 = x2) →
- (eq_option T f op1 op2 = true → op1 = op2).
- #T; #f; #op1; #op2; #H;
- nelim op1;
- nelim op2;
+ (∀op1,op2:option T.
+  (eq_option T f op1 op2 = true → op1 = op2)).
+ #T; #f; #H;
+ #op1; #op2; nelim op1; nelim op2;
  nnormalize;
  ##[ ##1: #H1; napply refl_eq
  ##| ##2,3: #a; #H1; ndestruct (*napply (bool_destruct … H1)*)
@@ -106,7 +106,9 @@ nlemma eqoption_to_eq :
  ##]
 nqed.
 
-nlemma decidable_option : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:option T.decidable (x = y).
+nlemma decidable_option :
+∀T.(Πx,y:T.decidable (x = y)) →
+   (∀x,y:option T.decidable (x = y)).
  #T; #H; #x; nelim x;
  ##[ ##1: #y; ncases y;
           ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
@@ -132,17 +134,18 @@ nlemma decidable_option : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:option T.
 nqed.
 
 nlemma neq_to_neqoption :
-∀T.∀f:T → T → bool.∀op1,op2:option T.
+∀T.∀f:T → T → bool.
  (∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) →
- (op1 ≠ op2 → eq_option T f op1 op2 = false).
- #T; #f; #op1; nelim op1;
+ (∀op1,op2:option T.
+  (op1 ≠ op2 → eq_option T f op1 op2 = false)).
+ #T; #f; #H; #op1; nelim op1;
  ##[ ##1: #op2; ncases op2;
-          ##[ ##1: nnormalize; #H; #H1; nelim (H1 (refl_eq …))
-          ##| ##2: #yy; #H; nnormalize; #H1; napply refl_eq
+          ##[ ##1: nnormalize; #H1; nelim (H1 (refl_eq …))
+          ##| ##2: #yy; nnormalize; #H1; napply refl_eq
           ##]
  ##| ##2: #xx; #op2; ncases op2;
-          ##[ ##1: #H; nnormalize; #H1; napply refl_eq
-          ##| ##2: #yy; #H; nnormalize; #H1; napply (H xx yy …);
+          ##[ ##1: nnormalize; #H1; napply refl_eq
+          ##| ##2: #yy; nnormalize; #H1; napply (H xx yy …);
                    nnormalize; #H2; nrewrite > H2 in H1:(%); #H1;
                    napply (H1 (refl_eq …))
           ##]
@@ -150,22 +153,23 @@ nlemma neq_to_neqoption :
 nqed.
 
 nlemma neqoption_to_neq :
-∀T.∀f:T → T → bool.∀op1,op2:option T.
+∀T.∀f:T → T → bool.
  (∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) →
- (eq_option T f op1 op2 = false → op1 ≠ op2).
- #T; #f; #op1; nelim op1;
+ (∀op1,op2:option T.
+  (eq_option T f op1 op2 = false → op1 ≠ op2)).
+ #T; #f; #H; #op1; nelim op1;
  ##[ ##1: #op2; ncases op2;
-          ##[ ##1: nnormalize; #H; #H1;
+          ##[ ##1: nnormalize; #H1;
                    ndestruct (*napply (bool_destruct … H1)*)
-          ##| ##2: #yy; #H; nnormalize; #H1; #H2;
+          ##| ##2: #yy; nnormalize; #H1; #H2;
                    (* !!! ndestruct: assert false *)
                    napply (option_destruct_none_some T … H2)
           ##]
  ##| ##2: #xx; #op2; ncases op2;
-          ##[ ##1: nnormalize; #H; #H1; #H2;
+          ##[ ##1: nnormalize; #H1; #H2;
                    (* !!! ndestruct: assert false *)
                    napply (option_destruct_some_none T … H2)
-          ##| ##2: #yy; #H; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
+          ##| ##2: #yy; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
                    napply (option_destruct_some_some T … H2)
           ##]
  ##]