X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fword16_lemmas.ma;h=06030fffb9ed0c5dae9f29052265261602722315;hb=29cfb9e2961e62c836cb50217905c0594a074e81;hp=a9c59de32ac9d21f11f2b4fc247d8ec46a5389fd;hpb=dc6723959a8e035e2935ca66bd3043de8eb11b42;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma
index a9c59de32..06030fffb 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma
@@ -342,12 +342,12 @@ nlemma decidable_w16 : ∀x,y:word16.decidable (x = y).
  #x; nelim x; #b1; #b2;
  #y; nelim y; #b3; #b4;
  nnormalize;
- napply (or_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
- ##[ ##2: #H; napply (or_intror … (decidable_w16_aux1 b1 b2 b3 b4 H))
- ##| ##1: #H; napply (or_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
-          ##[ ##2: #H1; napply (or_intror … (decidable_w16_aux2 b1 b2 b3 b4 H1))
+ napply (or2_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_w16_aux1 b1 b2 b3 b4 H))
+ ##| ##1: #H; napply (or2_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
+          ##[ ##2: #H1; napply (or2_intro2 … (decidable_w16_aux2 b1 b2 b3 b4 H1))
           ##| ##1: #H1; nrewrite > H; nrewrite > H1;
-                        napply (or_introl … (refl_eq ? 〈b3:b4〉))
+                        napply (or2_intro1 … (refl_eq ? 〈b3:b4〉))
           ##]
  ##]
 nqed.
@@ -359,7 +359,7 @@ nlemma neqw16_to_neq : ∀w1,w2:word16.(eq_w16 w1 w2 = false) → (w1 ≠ w2).
  #b1; #b2; #b3; #b4;
  nchange with ((((eq_b8 b3 b1) ⊗ (eq_b8 b4 b2)) = false) → ?);
  #H;
- napply (or_elim ((eq_b8 b3 b1) = false) ((eq_b8 b4 b2) = false) ? (andb_false … H) …);
+ napply (or2_elim ((eq_b8 b3 b1) = false) ((eq_b8 b4 b2) = false) ? (andb_false … H) …);
  ##[ ##1: #H1; napply (decidable_w16_aux1 … (neqb8_to_neq … H1))
  ##| ##2: #H1; napply (decidable_w16_aux2 … (neqb8_to_neq … H1))
  ##]
@@ -368,10 +368,10 @@ nqed.
 nlemma word16_destruct : ∀b1,b2,b3,b4.〈b1:b2〉 ≠ 〈b3:b4〉 → b1 ≠ b3 ∨ b2 ≠ b4.
  #b1; #b2; #b3; #b4;
  nnormalize; #H;
- napply (or_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
- ##[ ##2: #H1; napply (or_introl … H1)
- ##| ##1: #H1; napply (or_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
-          ##[ ##2: #H2; napply (or_intror … H2)
+ napply (or2_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
+ ##[ ##2: #H1; napply (or2_intro1 … H1)
+ ##| ##1: #H1; napply (or2_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
+          ##[ ##2: #H2; napply (or2_intro2 … H2)
           ##| ##1: #H2; nrewrite > H1 in H:(%);
                    nrewrite > H2;
                    #H; nelim (H (refl_eq …))
@@ -384,7 +384,7 @@ nlemma neq_to_neqw16 : ∀w1,w2.w1 ≠ w2 → eq_w16 w1 w2 = false.
  nelim w1; #b1; #b2;
  nelim w2; #b3; #b4;
  #H; nchange with (((eq_b8 b1 b3) ⊗ (eq_b8 b2 b4)) = false);
- napply (or_elim (b1 ≠ b3) (b2 ≠ b4) ? (word16_destruct … H) …);
+ napply (or2_elim (b1 ≠ b3) (b2 ≠ b4) ? (word16_destruct … H) …);
  ##[ ##1: #H1; nrewrite > (neq_to_neqb8 … H1); nnormalize; napply refl_eq
  ##| ##2: #H1; nrewrite > (neq_to_neqb8 … H1);
           nrewrite > (symmetric_andbool (eq_b8 b1 b3) false);