X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fquatern_lemmas.ma;h=00e559ed4b1b44b292fbcf0cb2cf777c51432278;hb=29cfb9e2961e62c836cb50217905c0594a074e81;hp=d32aa0f3e83321a3f3ca587424a15c1782f1a51a;hpb=5450fa91891df49587fedff6edd6179cf1bbc879;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma
index d32aa0f3e..00e559ed4 100755
--- a/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma
@@ -99,8 +99,8 @@ nlemma decidable_qu : ∀x,y:quatern.decidable (x = y).
  nnormalize;
  nelim x;
  nelim y;
- ##[ ##1,6,11,16: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (quatern_destruct … H)
+ ##[ ##1,6,11,16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (quatern_destruct … H)
  ##]
 nqed.