X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fopcodes%2FIP2022_instr_mode_lemmas.ma;h=7538086c166290ac0f7ee04284cea46072addb77;hb=ced2abc1e3fe84d5bbfa9ccb2ebf46f253279ebe;hp=eb7f9b820dea7aefefbe3dd70f415013da066cfc;hpb=d6a9ed2a08fcc4e3e26a40cde8cab88c2c69cb3a;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode_lemmas.ma b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode_lemmas.ma
index eb7f9b820..7538086c1 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/opcodes/IP2022_instr_mode_lemmas.ma
@@ -29,8 +29,8 @@ nlemma eq_to_eqIP2022im : ∀n1,n2.n1 = n2 → eq_IP2022_im n1 n2 = true.
  #n1; #n2; #H;
  nrewrite > H;
  nelim n2;
- ##[ ##2,9,10: #o; nrewrite > (eq_to_eqoct … (refl_eq …))
- ##| ##4: #t; nrewrite > (eq_to_eqbit … (refl_eq …)) ##]
+ ##[ ##4,11,12: #o; nrewrite > (eq_to_eqoct … (refl_eq …))
+ ##| ##6: #t; nrewrite > (eq_to_eqbit … (refl_eq …)) ##]
  nnormalize;
  napply refl_eq.
 nqed.