X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fstatus_lemmas.ma;h=9edad75cc6c025d7315a6a4e06d5dcc2e7c35184;hb=601baed778a190b580982b588ebe49ba3f762b30;hp=568590e19810524cdfeb5ea30fa2e7460611f533;hpb=a687cf5e3e9ae6fb6ead058c4a191002f21fa951;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma
index 568590e19..9edad75cc 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma
@@ -15,16 +15,16 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
-include "freescale/word16_lemmas.ma".
+include "num/word16_lemmas.ma".
 include "freescale/opcode_base_lemmas1.ma".
 include "freescale/status.ma".
-include "freescale/option_lemmas.ma".
-include "freescale/prod_lemmas.ma".
+include "common/option_lemmas.ma".
+include "common/prod_lemmas.ma".
 
 (* *********************************** *)
 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
@@ -40,7 +40,7 @@ nlemma aluHC05_destruct_1 :
                 with [ mk_alu_HC05 a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC05_destruct_2 :
@@ -53,7 +53,7 @@ nlemma aluHC05_destruct_2 :
                 with [ mk_alu_HC05 _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC05_destruct_3 :
@@ -66,7 +66,7 @@ nlemma aluHC05_destruct_3 :
                 with [ mk_alu_HC05 _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC05_destruct_4 :
@@ -79,7 +79,7 @@ nlemma aluHC05_destruct_4 :
                 with [ mk_alu_HC05 _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC05_destruct_5 :
@@ -92,7 +92,7 @@ nlemma aluHC05_destruct_5 :
                 with [ mk_alu_HC05 _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC05_destruct_6 :
@@ -105,7 +105,7 @@ nlemma aluHC05_destruct_6 :
                 with [ mk_alu_HC05 _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x6 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC05_destruct_7 :
@@ -118,7 +118,7 @@ nlemma aluHC05_destruct_7 :
                 with [ mk_alu_HC05 _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x7 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC05_destruct_8 :
@@ -131,7 +131,7 @@ nlemma aluHC05_destruct_8 :
                 with [ mk_alu_HC05 _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x8 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC05_destruct_9 :
@@ -144,7 +144,7 @@ nlemma aluHC05_destruct_9 :
                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x9 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC05_destruct_10 :
@@ -157,7 +157,7 @@ nlemma aluHC05_destruct_10 :
                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x10 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC05_destruct_11 :
@@ -170,7 +170,7 @@ nlemma aluHC05_destruct_11 :
                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x11 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC05_destruct_12 :
@@ -183,7 +183,7 @@ nlemma aluHC05_destruct_12 :
                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x12 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC05_destruct_13 :
@@ -196,7 +196,7 @@ nlemma aluHC05_destruct_13 :
                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x13 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_alu_HC05.
@@ -226,7 +226,7 @@ nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_alu_HC05.
  nrewrite > (symmetric_eqbool x11 y11);
  nrewrite > (symmetric_eqbool x12 y12);
  nrewrite > (symmetric_eqbool x13 y13);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_alu_HC05 alu1 alu2 = true → alu1 = alu2.
@@ -243,31 +243,31 @@ nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_alu_HC05 alu1 alu2 = true → alu1 = al
   (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗
   (eq_bool x11 y11) ⊗ (eq_bool x12 y12) ⊗
   (eq_bool x13 y13)) = true);  
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H));
- nletin H1 ≝ (andb_true_true_l ?? H);
- nrewrite > (eqbool_to_eq x12 y12 (andb_true_true_r ?? (andb_true_true_l ?? H)));
- nletin H2 ≝ (andb_true_true_l ?? H1);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H2));
- nletin H3 ≝ (andb_true_true_l ?? H2);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H3));
- nletin H4 ≝ (andb_true_true_l ?? H3);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H4));
- nletin H5 ≝ (andb_true_true_l ?? H4);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H5));
- nletin H6 ≝ (andb_true_true_l ?? H5);
- nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H6));
- nletin H7 ≝ (andb_true_true_l ?? H6);
- nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H7));
- nletin H8 ≝ (andb_true_true_l ?? H7);
- nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H8));
- nletin H9 ≝ (andb_true_true_l ?? H8);
- nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H9));
- nletin H10 ≝ (andb_true_true_l ?? H9);
- nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H10));
- nletin H11 ≝ (andb_true_true_l ?? H10);
- nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H11));
- nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H11));
- napply (refl_eq ??).
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
+ nletin H1 ≝ (andb_true_true_l … H);
+ nrewrite > (eqbool_to_eq x12 y12 (andb_true_true_r … (andb_true_true_l … H)));
+ nletin H2 ≝ (andb_true_true_l … H1);
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H2));
+ nletin H3 ≝ (andb_true_true_l … H2);
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H3));
+ nletin H4 ≝ (andb_true_true_l … H3);
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H4));
+ nletin H5 ≝ (andb_true_true_l … H4);
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H5));
+ nletin H6 ≝ (andb_true_true_l … H5);
+ nrewrite > (eqw16_to_eq … (andb_true_true_r … H6));
+ nletin H7 ≝ (andb_true_true_l … H6);
+ nrewrite > (eqw16_to_eq … (andb_true_true_r … H7));
+ nletin H8 ≝ (andb_true_true_l … H7);
+ nrewrite > (eqw16_to_eq … (andb_true_true_r … H8));
+ nletin H9 ≝ (andb_true_true_l … H8);
+ nrewrite > (eqw16_to_eq … (andb_true_true_r … H9));
+ nletin H10 ≝ (andb_true_true_l … H9);
+ nrewrite > (eqw16_to_eq … (andb_true_true_r … H10));
+ nletin H11 ≝ (andb_true_true_l … H10);
+ nrewrite > (eqb8_to_eq … (andb_true_true_r … H11));
+ nrewrite > (eqb8_to_eq … (andb_true_true_l … H11));
+ napply refl_eq.
 nqed.
 
 nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC05 alu1 alu2 = true.
@@ -276,19 +276,19 @@ nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC05 alu1 alu2 = tr
  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  ncases alu2;
  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
- nrewrite > (aluHC05_destruct_1 ?????????????????????????? H);
- nrewrite > (aluHC05_destruct_2 ?????????????????????????? H);
- nrewrite > (aluHC05_destruct_3 ?????????????????????????? H);
- nrewrite > (aluHC05_destruct_4 ?????????????????????????? H);
- nrewrite > (aluHC05_destruct_5 ?????????????????????????? H);
- nrewrite > (aluHC05_destruct_6 ?????????????????????????? H);
- nrewrite > (aluHC05_destruct_7 ?????????????????????????? H);
- nrewrite > (aluHC05_destruct_8 ?????????????????????????? H);
- nrewrite > (aluHC05_destruct_9 ?????????????????????????? H);
- nrewrite > (aluHC05_destruct_10 ?????????????????????????? H);
- nrewrite > (aluHC05_destruct_11 ?????????????????????????? H);
- nrewrite > (aluHC05_destruct_12 ?????????????????????????? H);
- nrewrite > (aluHC05_destruct_13 ?????????????????????????? H);
+ nrewrite > (aluHC05_destruct_1 … H);
+ nrewrite > (aluHC05_destruct_2 … H);
+ nrewrite > (aluHC05_destruct_3 … H);
+ nrewrite > (aluHC05_destruct_4 … H);
+ nrewrite > (aluHC05_destruct_5 … H);
+ nrewrite > (aluHC05_destruct_6 … H);
+ nrewrite > (aluHC05_destruct_7 … H);
+ nrewrite > (aluHC05_destruct_8 … H);
+ nrewrite > (aluHC05_destruct_9 … H);
+ nrewrite > (aluHC05_destruct_10 … H);
+ nrewrite > (aluHC05_destruct_11 … H);
+ nrewrite > (aluHC05_destruct_12 … H);
+ nrewrite > (aluHC05_destruct_13 … H);
  nchange with (
  ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗
   (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
@@ -297,20 +297,20 @@ nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC05 alu1 alu2 = tr
   (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗
   (eq_bool y11 y11) ⊗ (eq_bool y12 y12) ⊗
   (eq_bool y13 y13)) = true); 
- nrewrite > (eq_to_eqb8 y1 y1 (refl_eq ??));
- nrewrite > (eq_to_eqb8 y2 y2 (refl_eq ??));
- nrewrite > (eq_to_eqw16 y3 y3 (refl_eq ??));
- nrewrite > (eq_to_eqw16 y4 y4 (refl_eq ??));
- nrewrite > (eq_to_eqw16 y5 y5 (refl_eq ??));
- nrewrite > (eq_to_eqw16 y6 y6 (refl_eq ??));
- nrewrite > (eq_to_eqw16 y7 y7 (refl_eq ??));
- nrewrite > (eq_to_eqbool y8 y8 (refl_eq ??));
- nrewrite > (eq_to_eqbool y9 y9 (refl_eq ??));
- nrewrite > (eq_to_eqbool y10 y10 (refl_eq ??));
- nrewrite > (eq_to_eqbool y11 y11 (refl_eq ??));
- nrewrite > (eq_to_eqbool y12 y12 (refl_eq ??));
- nrewrite > (eq_to_eqbool y13 y13 (refl_eq ??));
- napply (refl_eq ??).
+ nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
+ nrewrite > (eq_to_eqb8 y2 y2 (refl_eq …));
+ nrewrite > (eq_to_eqw16 y3 y3 (refl_eq …));
+ nrewrite > (eq_to_eqw16 y4 y4 (refl_eq …));
+ nrewrite > (eq_to_eqw16 y5 y5 (refl_eq …));
+ nrewrite > (eq_to_eqw16 y6 y6 (refl_eq …));
+ nrewrite > (eq_to_eqw16 y7 y7 (refl_eq …));
+ nrewrite > (eq_to_eqbool y8 y8 (refl_eq …));
+ nrewrite > (eq_to_eqbool y9 y9 (refl_eq …));
+ nrewrite > (eq_to_eqbool y10 y10 (refl_eq …));
+ nrewrite > (eq_to_eqbool y11 y11 (refl_eq …));
+ nrewrite > (eq_to_eqbool y12 y12 (refl_eq …));
+ nrewrite > (eq_to_eqbool y13 y13 (refl_eq …));
+ napply refl_eq.
 nqed.
 
 nlemma aluHC08_destruct_1 :
@@ -323,7 +323,7 @@ nlemma aluHC08_destruct_1 :
                 with [ mk_alu_HC08 a _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC08_destruct_2 :
@@ -336,7 +336,7 @@ nlemma aluHC08_destruct_2 :
                 with [ mk_alu_HC08 _ a _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC08_destruct_3 :
@@ -349,7 +349,7 @@ nlemma aluHC08_destruct_3 :
                 with [ mk_alu_HC08 _ _ a _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC08_destruct_4 :
@@ -362,7 +362,7 @@ nlemma aluHC08_destruct_4 :
                 with [ mk_alu_HC08 _ _ _ a _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC08_destruct_5 :
@@ -375,7 +375,7 @@ nlemma aluHC08_destruct_5 :
                 with [ mk_alu_HC08 _ _ _ _ a _ _ _ _ _ _ _ ⇒ x5 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC08_destruct_6 :
@@ -388,7 +388,7 @@ nlemma aluHC08_destruct_6 :
                 with [ mk_alu_HC08 _ _ _ _ _ a _ _ _ _ _ _ ⇒ x6 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC08_destruct_7 :
@@ -401,7 +401,7 @@ nlemma aluHC08_destruct_7 :
                 with [ mk_alu_HC08 _ _ _ _ _ _ a _ _ _ _ _ ⇒ x7 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC08_destruct_8 :
@@ -414,7 +414,7 @@ nlemma aluHC08_destruct_8 :
                 with [ mk_alu_HC08 _ _ _ _ _ _ _ a _ _ _ _ ⇒ x8 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC08_destruct_9 :
@@ -427,7 +427,7 @@ nlemma aluHC08_destruct_9 :
                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ a _ _ _ ⇒ x9 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC08_destruct_10 :
@@ -440,7 +440,7 @@ nlemma aluHC08_destruct_10 :
                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ a _ _ ⇒ x10 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC08_destruct_11 :
@@ -453,7 +453,7 @@ nlemma aluHC08_destruct_11 :
                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ a _ ⇒ x11 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluHC08_destruct_12 :
@@ -466,7 +466,7 @@ nlemma aluHC08_destruct_12 :
                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ _ a ⇒ x12 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_alu_HC08.
@@ -494,7 +494,7 @@ nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_alu_HC08.
  nrewrite > (symmetric_eqbool x10 y10);
  nrewrite > (symmetric_eqbool x11 y11);
  nrewrite > (symmetric_eqbool x12 y12);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_alu_HC08 alu1 alu2 = true → alu1 = alu2.
@@ -507,29 +507,29 @@ nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_alu_HC08 alu1 alu2 = true → alu1 = al
  ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_b8 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
   (eq_w16 x5 y5) ⊗ (eq_bool x6 y6) ⊗ (eq_bool x7 y7) ⊗ (eq_bool x8 y8) ⊗
   (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12)) = true);  
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H));
- nletin H1 ≝ (andb_true_true_l ?? H);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H1));
- nletin H2 ≝ (andb_true_true_l ?? H1);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H2));
- nletin H3 ≝ (andb_true_true_l ?? H2);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H3));
- nletin H4 ≝ (andb_true_true_l ?? H3);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H4));
- nletin H5 ≝ (andb_true_true_l ?? H4);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H5));
- nletin H6 ≝ (andb_true_true_l ?? H5);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H6));
- nletin H7 ≝ (andb_true_true_l ?? H6);
- nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H7));
- nletin H8 ≝ (andb_true_true_l ?? H7);
- nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H8));
- nletin H9 ≝ (andb_true_true_l ?? H8);
- nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H9));
- nletin H10 ≝ (andb_true_true_l ?? H9);
- nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H10));
- nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H10));
- napply (refl_eq ??).
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
+ nletin H1 ≝ (andb_true_true_l … H);
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H1));
+ nletin H2 ≝ (andb_true_true_l … H1);
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H2));
+ nletin H3 ≝ (andb_true_true_l … H2);
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H3));
+ nletin H4 ≝ (andb_true_true_l … H3);
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H4));
+ nletin H5 ≝ (andb_true_true_l … H4);
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H5));
+ nletin H6 ≝ (andb_true_true_l … H5);
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H6));
+ nletin H7 ≝ (andb_true_true_l … H6);
+ nrewrite > (eqw16_to_eq … (andb_true_true_r … H7));
+ nletin H8 ≝ (andb_true_true_l … H7);
+ nrewrite > (eqw16_to_eq … (andb_true_true_r … H8));
+ nletin H9 ≝ (andb_true_true_l … H8);
+ nrewrite > (eqb8_to_eq … (andb_true_true_r … H9));
+ nletin H10 ≝ (andb_true_true_l … H9);
+ nrewrite > (eqb8_to_eq … (andb_true_true_r … H10));
+ nrewrite > (eqb8_to_eq … (andb_true_true_l … H10));
+ napply refl_eq.
 nqed.
 
 nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC08 alu1 alu2 = true.
@@ -538,35 +538,35 @@ nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC08 alu1 alu2 = tr
  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
  ncases alu2;
  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
- nrewrite > (aluHC08_destruct_1 ???????????????????????? H);
- nrewrite > (aluHC08_destruct_2 ???????????????????????? H);
- nrewrite > (aluHC08_destruct_3 ???????????????????????? H);
- nrewrite > (aluHC08_destruct_4 ???????????????????????? H);
- nrewrite > (aluHC08_destruct_5 ???????????????????????? H);
- nrewrite > (aluHC08_destruct_6 ???????????????????????? H);
- nrewrite > (aluHC08_destruct_7 ???????????????????????? H);
- nrewrite > (aluHC08_destruct_8 ???????????????????????? H);
- nrewrite > (aluHC08_destruct_9 ???????????????????????? H);
- nrewrite > (aluHC08_destruct_10 ???????????????????????? H);
- nrewrite > (aluHC08_destruct_11 ???????????????????????? H);
- nrewrite > (aluHC08_destruct_12 ???????????????????????? H);
+ nrewrite > (aluHC08_destruct_1 … H);
+ nrewrite > (aluHC08_destruct_2 … H);
+ nrewrite > (aluHC08_destruct_3 … H);
+ nrewrite > (aluHC08_destruct_4 … H);
+ nrewrite > (aluHC08_destruct_5 … H);
+ nrewrite > (aluHC08_destruct_6 … H);
+ nrewrite > (aluHC08_destruct_7 … H);
+ nrewrite > (aluHC08_destruct_8 … H);
+ nrewrite > (aluHC08_destruct_9 … H);
+ nrewrite > (aluHC08_destruct_10 … H);
+ nrewrite > (aluHC08_destruct_11 … H);
+ nrewrite > (aluHC08_destruct_12 … H);
  nchange with (
  ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗ (eq_b8 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
   (eq_w16 y5 y5) ⊗ (eq_bool y6 y6) ⊗ (eq_bool y7 y7) ⊗ (eq_bool y8 y8) ⊗
   (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗ (eq_bool y11 y11) ⊗ (eq_bool y12 y12)) = true); 
- nrewrite > (eq_to_eqb8 y1 y1 (refl_eq ??));
- nrewrite > (eq_to_eqb8 y2 y2 (refl_eq ??));
- nrewrite > (eq_to_eqb8 y3 y3 (refl_eq ??));
- nrewrite > (eq_to_eqw16 y4 y4 (refl_eq ??));
- nrewrite > (eq_to_eqw16 y5 y5 (refl_eq ??));
- nrewrite > (eq_to_eqbool y6 y6 (refl_eq ??));
- nrewrite > (eq_to_eqbool y7 y7 (refl_eq ??));
- nrewrite > (eq_to_eqbool y8 y8 (refl_eq ??));
- nrewrite > (eq_to_eqbool y9 y9 (refl_eq ??));
- nrewrite > (eq_to_eqbool y10 y10 (refl_eq ??));
- nrewrite > (eq_to_eqbool y11 y11 (refl_eq ??));
- nrewrite > (eq_to_eqbool y12 y12 (refl_eq ??));
- napply (refl_eq ??).
+ nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
+ nrewrite > (eq_to_eqb8 y2 y2 (refl_eq …));
+ nrewrite > (eq_to_eqb8 y3 y3 (refl_eq …));
+ nrewrite > (eq_to_eqw16 y4 y4 (refl_eq …));
+ nrewrite > (eq_to_eqw16 y5 y5 (refl_eq …));
+ nrewrite > (eq_to_eqbool y6 y6 (refl_eq …));
+ nrewrite > (eq_to_eqbool y7 y7 (refl_eq …));
+ nrewrite > (eq_to_eqbool y8 y8 (refl_eq …));
+ nrewrite > (eq_to_eqbool y9 y9 (refl_eq …));
+ nrewrite > (eq_to_eqbool y10 y10 (refl_eq …));
+ nrewrite > (eq_to_eqbool y11 y11 (refl_eq …));
+ nrewrite > (eq_to_eqbool y12 y12 (refl_eq …));
+ napply refl_eq.
 nqed.
 
 nlemma aluRS08_destruct_1 :
@@ -579,7 +579,7 @@ nlemma aluRS08_destruct_1 :
                 with [ mk_alu_RS08 a _ _ _ _ _ _ _ ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluRS08_destruct_2 :
@@ -592,7 +592,7 @@ nlemma aluRS08_destruct_2 :
                 with [ mk_alu_RS08 _ a _ _ _ _ _ _ ⇒ x2 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluRS08_destruct_3 :
@@ -605,7 +605,7 @@ nlemma aluRS08_destruct_3 :
                 with [ mk_alu_RS08 _ _ a _ _ _ _ _ ⇒ x3 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluRS08_destruct_4 :
@@ -618,7 +618,7 @@ nlemma aluRS08_destruct_4 :
                 with [ mk_alu_RS08 _ _ _ a _ _ _ _ ⇒ x4 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluRS08_destruct_5 :
@@ -631,7 +631,7 @@ nlemma aluRS08_destruct_5 :
                 with [ mk_alu_RS08 _ _ _ _ a _ _ _ ⇒ x5 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluRS08_destruct_6 :
@@ -644,7 +644,7 @@ nlemma aluRS08_destruct_6 :
                 with [ mk_alu_RS08 _ _ _ _ _ a _ _ ⇒ x6 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluRS08_destruct_7 :
@@ -657,7 +657,7 @@ nlemma aluRS08_destruct_7 :
                 with [ mk_alu_RS08 _ _ _ _ _ _ a _ ⇒ x7 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma aluRS08_destruct_8 :
@@ -670,7 +670,7 @@ nlemma aluRS08_destruct_8 :
                 with [ mk_alu_RS08 _ _ _ _ _ _ _ a ⇒ x8 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_alu_RS08.
@@ -696,7 +696,7 @@ nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_alu_RS08.
  nrewrite > (symmetric_eqb8 x6 y6);
  nrewrite > (symmetric_eqbool x7 y7);
  nrewrite > (symmetric_eqbool x8 y8);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_alu_RS08 alu1 alu2 = true → alu1 = alu2.
@@ -710,21 +710,21 @@ nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_alu_RS08 alu1 alu2 = true → alu1 = al
    (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
    (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
    (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) = true);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H));
- nletin H1 ≝ (andb_true_true_l ?? H);
- nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H1));
- nletin H2 ≝ (andb_true_true_l ?? H1);
- nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H2));
- nletin H3 ≝ (andb_true_true_l ?? H2);
- nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H3));
- nletin H4 ≝ (andb_true_true_l ?? H3);
- nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H4));
- nletin H5 ≝ (andb_true_true_l ?? H4);
- nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H5));
- nletin H6 ≝ (andb_true_true_l ?? H5);
- nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H6));
- nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H6));
- napply (refl_eq ??).
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
+ nletin H1 ≝ (andb_true_true_l … H);
+ nrewrite > (eqbool_to_eq … (andb_true_true_r … H1));
+ nletin H2 ≝ (andb_true_true_l … H1);
+ nrewrite > (eqb8_to_eq … (andb_true_true_r … H2));
+ nletin H3 ≝ (andb_true_true_l … H2);
+ nrewrite > (eqb8_to_eq … (andb_true_true_r … H3));
+ nletin H4 ≝ (andb_true_true_l … H3);
+ nrewrite > (eqw16_to_eq … (andb_true_true_r … H4));
+ nletin H5 ≝ (andb_true_true_l … H4);
+ nrewrite > (eqw16_to_eq … (andb_true_true_r … H5));
+ nletin H6 ≝ (andb_true_true_l … H5);
+ nrewrite > (eqw16_to_eq … (andb_true_true_r … H6));
+ nrewrite > (eqb8_to_eq … (andb_true_true_l … H6));
+ napply refl_eq.
 nqed.
 
 nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_RS08 alu1 alu2 = true.
@@ -733,47 +733,47 @@ nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_RS08 alu1 alu2 = tr
  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
  ncases alu2;
  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
- nrewrite > (aluRS08_destruct_1 ???????????????? H);
- nrewrite > (aluRS08_destruct_2 ???????????????? H);
- nrewrite > (aluRS08_destruct_3 ???????????????? H);
- nrewrite > (aluRS08_destruct_4 ???????????????? H);
- nrewrite > (aluRS08_destruct_5 ???????????????? H);
- nrewrite > (aluRS08_destruct_6 ???????????????? H);
- nrewrite > (aluRS08_destruct_7 ???????????????? H);
- nrewrite > (aluRS08_destruct_8 ???????????????? H);
+ nrewrite > (aluRS08_destruct_1 … H);
+ nrewrite > (aluRS08_destruct_2 … H);
+ nrewrite > (aluRS08_destruct_3 … H);
+ nrewrite > (aluRS08_destruct_4 … H);
+ nrewrite > (aluRS08_destruct_5 … H);
+ nrewrite > (aluRS08_destruct_6 … H);
+ nrewrite > (aluRS08_destruct_7 … H);
+ nrewrite > (aluRS08_destruct_8 … H);
  nchange with (
   ((eq_b8 y1 y1) ⊗ (eq_w16 y2 y2) ⊗
    (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
    (eq_b8 y5 y5) ⊗ (eq_b8 y6 y6) ⊗
    (eq_bool y7 y7) ⊗ (eq_bool y8 y8)) = true);
- nrewrite > (eq_to_eqb8 y1 y1 (refl_eq ??));
- nrewrite > (eq_to_eqw16 y2 y2 (refl_eq ??));
- nrewrite > (eq_to_eqw16 y3 y3 (refl_eq ??));
- nrewrite > (eq_to_eqw16 y4 y4 (refl_eq ??));
- nrewrite > (eq_to_eqb8 y5 y5 (refl_eq ??));
- nrewrite > (eq_to_eqb8 y6 y6 (refl_eq ??));
- nrewrite > (eq_to_eqbool y7 y7 (refl_eq ??));
- nrewrite > (eq_to_eqbool y8 y8 (refl_eq ??));
- napply (refl_eq ??).
+ nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
+ nrewrite > (eq_to_eqw16 y2 y2 (refl_eq …));
+ nrewrite > (eq_to_eqw16 y3 y3 (refl_eq …));
+ nrewrite > (eq_to_eqw16 y4 y4 (refl_eq …));
+ nrewrite > (eq_to_eqb8 y5 y5 (refl_eq …));
+ nrewrite > (eq_to_eqb8 y6 y6 (refl_eq …));
+ nrewrite > (eq_to_eqbool y7 y7 (refl_eq …));
+ nrewrite > (eq_to_eqbool y8 y8 (refl_eq …));
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_eqclk : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = eq_clk mcu clk2 clk1.
  #mcu; #clk1; #clk2;
  ncases clk1;
  ncases clk2;
- ##[ ##1: napply (refl_eq ??)
- ##| ##2,3: nnormalize; #H; napply (refl_eq ??)
+ ##[ ##1: napply refl_eq
+ ##| ##2,3: nnormalize; #H; napply refl_eq
  ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
           #p2; ncases p2; #y1; #y2; #y3; #y4; #y5;
           nchange with (
-           ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_instrmode y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) =
-           ((eq_b8 x1 y1) ⊗ (eq_anyop ? x2 y2) ⊗ (eq_instrmode x3 y3) ⊗ (eq_b8 x4 y4) ⊗ (eq_w16 x5 y5)));
+           ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_im y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) =
+           ((eq_b8 x1 y1) ⊗ (eq_anyop ? x2 y2) ⊗ (eq_im x3 y3) ⊗ (eq_b8 x4 y4) ⊗ (eq_w16 x5 y5)));
           nrewrite > (symmetric_eqb8 x1 y1);
           nrewrite > (symmetric_eqanyop ? x2 y2);
-          nrewrite > (symmetric_eqinstrmode x3 y3);
+          nrewrite > (symmetric_eqim x3 y3);
           nrewrite > (symmetric_eqb8 x4 y4);
           nrewrite > (symmetric_eqw16 x5 y5);
-          napply (refl_eq ??)
+          napply refl_eq
  ##]
 nqed.
 
@@ -781,21 +781,21 @@ nlemma eqclk_to_eq : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = true → clk1 = clk
  #mcu; #clk1; #clk2;
  ncases clk1;
  ncases clk2;
- ##[ ##1: nnormalize; #H; napply (refl_eq ??)
- ##| ##2,3: nnormalize; #H; #H1; napply (bool_destruct ??? H1)
+ ##[ ##1: nnormalize; #H; napply refl_eq
+ ##| ##2,3: nnormalize; #H; #H1; napply (bool_destruct … H1)
  ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
           #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
           nchange in H:(%) with (
-           ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_instrmode y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) = true);
-           nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H));
-           nletin H1 ≝ (andb_true_true_l ?? H);
-           nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H1));
-           nletin H2 ≝ (andb_true_true_l ?? H1);
-           nrewrite > (eqinstrmode_to_eq ?? (andb_true_true_r ?? H2));
-           nletin H3 ≝ (andb_true_true_l ?? H2);
-           nrewrite > (eqanyop_to_eq ??? (andb_true_true_r ?? H3));
-           nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H3));
-           napply (refl_eq ??)
+           ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_im y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) = true);
+           nrewrite > (eqw16_to_eq … (andb_true_true_r … H));
+           nletin H1 ≝ (andb_true_true_l … H);
+           nrewrite > (eqb8_to_eq … (andb_true_true_r … H1));
+           nletin H2 ≝ (andb_true_true_l … H1);
+           nrewrite > (eqim_to_eq … (andb_true_true_r … H2));
+           nletin H3 ≝ (andb_true_true_l … H2);
+           nrewrite > (eqanyop_to_eq … (andb_true_true_r … H3));
+           nrewrite > (eqb8_to_eq … (andb_true_true_l … H3));
+           napply refl_eq
  ##]
 nqed.
 
@@ -803,25 +803,25 @@ nlemma eq_to_eqclk : ∀mcu,clk1,clk2.clk1 = clk2 → eq_clk mcu clk1 clk2 = tru
  #mcu; #clk1; #clk2;
  ncases clk1;
  ncases clk2;
- ##[ ##1: nnormalize; #H; napply (refl_eq ??)
- ##| ##2: nnormalize; #p; #H1; nelim (option_destruct_none_some ?? H1)
- ##| ##3: nnormalize; #p; #H1; nelim (option_destruct_some_none ?? H1)
+ ##[ ##1: nnormalize; #H; napply refl_eq
+ ##| ##2: nnormalize; #p; #H1; nelim (option_destruct_none_some ? p … H1)
+ ##| ##3: nnormalize; #p; #H1; nelim (option_destruct_some_none ? p … H1)
  ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
           #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
-          nrewrite > (quintuple_destruct_1 ??????????????? (option_destruct_some_some ??? H));
-          nrewrite > (quintuple_destruct_2 ??????????????? (option_destruct_some_some ??? H));
-          nrewrite > (quintuple_destruct_3 ??????????????? (option_destruct_some_some ??? H));
-          nrewrite > (quintuple_destruct_4 ??????????????? (option_destruct_some_some ??? H));
-          nrewrite > (quintuple_destruct_5 ??????????????? (option_destruct_some_some ??? H));
+          nrewrite > (quintuple_destruct_1 … (option_destruct_some_some … H));
+          nrewrite > (quintuple_destruct_2 … (option_destruct_some_some … H));
+          nrewrite > (quintuple_destruct_3 … (option_destruct_some_some … H));
+          nrewrite > (quintuple_destruct_4 … (option_destruct_some_some … H));
+          nrewrite > (quintuple_destruct_5 … (option_destruct_some_some … H));
           nchange with (
-           ((eq_b8 x1 x1) ⊗ (eq_anyop ? x2 x2) ⊗ (eq_instrmode x3 x3) ⊗ (eq_b8 x4 x4) ⊗ (eq_w16 x5 x5)) = true);
-          nrewrite > (eq_to_eqb8 x1 x1 (refl_eq ??));
+           ((eq_b8 x1 x1) ⊗ (eq_anyop ? x2 x2) ⊗ (eq_im x3 x3) ⊗ (eq_b8 x4 x4) ⊗ (eq_w16 x5 x5)) = true);
+          nrewrite > (eq_to_eqb8 x1 x1 (refl_eq …));
           nrewrite > (eq_to_eqanyop mcu x2 x2 (refl_eq ? x2));
-          nrewrite > (eq_to_eqinstrmode x3 x3 (refl_eq ??));
-          nrewrite > (eq_to_eqb8 x4 x4 (refl_eq ??));
-          nrewrite > (eq_to_eqw16 x5 x5 (refl_eq ??));
+          nrewrite > (eq_to_eqim x3 x3 (refl_eq …));
+          nrewrite > (eq_to_eqb8 x4 x4 (refl_eq …));
+          nrewrite > (eq_to_eqw16 x5 x5 (refl_eq …));
           nnormalize;
-          napply (refl_eq ??)
+          napply refl_eq
  ##]
 nqed.
 
@@ -830,8 +830,8 @@ nlemma symmetric_forallmemoryranged :
  forall_memory_ranged t chk1 chk2 mem1 mem2 addrl =
  forall_memory_ranged t chk2 chk1 mem2 mem1 addrl.
  #t; #chk1; #chk2; #mem1; #mem2; #addrl;
- napply (list_ind word16 ??? addrl);
- ##[ ##1: nnormalize; napply (refl_eq ??)
+ napply (list_ind word16 … addrl);
+ ##[ ##1: nnormalize; napply refl_eq
  ##| ##2: #a; #l; #H;
           nchange with (
            ((eq_option byte8 (mem_read t mem1 chk1 a)
@@ -842,7 +842,7 @@ nlemma symmetric_forallmemoryranged :
            (forall_memory_ranged t chk2 chk1 mem2 mem1 l)));
            nrewrite > H;
            nrewrite > (symmetric_eqoption ? (mem_read t mem1 chk1 a) (mem_read t mem2 chk2 a) eq_b8 symmetric_eqb8);
-           napply (refl_eq ??)
+           napply refl_eq
  ##]
 nqed.
 
@@ -857,7 +857,7 @@ nlemma anystatus_destruct_1 :
                 with [ mk_any_status a _ _ _ ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma anystatus_destruct_2 :
@@ -871,7 +871,7 @@ nlemma anystatus_destruct_2 :
                 with [ mk_any_status _ a _ _ ⇒ x2 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma anystatus_destruct_3 :
@@ -885,7 +885,7 @@ nlemma anystatus_destruct_3 :
                 with [ mk_any_status _ _ a _ ⇒ x3 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma anystatus_destruct_4 :
@@ -899,7 +899,7 @@ nlemma anystatus_destruct_4 :
                 with [ mk_any_status _ _ _ a ⇒ x4 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_eqstatus :
@@ -928,7 +928,7 @@ nlemma symmetric_eqstatus :
  ##]
  nrewrite > (symmetric_forallmemoryranged t x3 y3 x2 y2 addrl);
  nrewrite > (symmetric_eqclk ? x4 y4);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma eqstatus_to_eq :
@@ -944,22 +944,22 @@ nlemma eqstatus_to_eq :
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
           nchange in H:(%) with (
            ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
-           nrewrite > (eqaluHC05_to_eq ?? (andb_true_true_l ?? (andb_true_true_l ?? H)))
+           nrewrite > (eqaluHC05_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
  ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
           nchange in H:(%) with (
            ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
-           nrewrite > (eqaluHC08_to_eq ?? (andb_true_true_l ?? (andb_true_true_l ?? H)))
+           nrewrite > (eqaluHC08_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
  ##| ##4: ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
           nchange in H:(%) with (
            ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
-           nrewrite > (eqaluRS08_to_eq ?? (andb_true_true_l ?? (andb_true_true_l ?? H)))
+           nrewrite > (eqaluRS08_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
  ##]
  nchange with ((y1 = y1) ∧ (x4 = y4) ∧ (forall_memory_ranged t x3 y3 x2 y2 addrl = true));
- nrewrite > (andb_true_true_r ?? (andb_true_true_l ?? H));
- nrewrite > (eqclk_to_eq ??? (andb_true_true_r ?? H));
- napply (conj ?? (conj ?? (refl_eq ??) (refl_eq ??)) (refl_eq ??)).
+ nrewrite > (andb_true_true_r … (andb_true_true_l … H));
+ nrewrite > (eqclk_to_eq … (andb_true_true_r … H));
+ napply (conj … (conj … (refl_eq ? y1) (refl_eq ? y4)) (refl_eq ? true)).
 nqed.
 
 nlemma eq_to_eqstatus_strong :
@@ -971,39 +971,39 @@ nlemma eq_to_eqstatus_strong :
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
           nchange with (
            ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
-          nrewrite > (anystatus_destruct_1 ?????????? H);
-          nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq ??))
+          nrewrite > (anystatus_destruct_1 … H);
+          nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq …))
  ##| ##2,3:  #s1; ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
           nchange with (
            ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
-          nrewrite > (anystatus_destruct_1 ?????????? H);
-          nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq ??))
+          nrewrite > (anystatus_destruct_1 … H);
+          nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq …))
  ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
           nchange with (
            ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
-          nrewrite > (anystatus_destruct_1 ?????????? H);
-          nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq ??))
+          nrewrite > (anystatus_destruct_1 … H);
+          nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq …))
  ##]
- nrewrite > (anystatus_destruct_2 ?????????? H);
- nrewrite > (anystatus_destruct_3 ?????????? H);
- nrewrite > (anystatus_destruct_4 ?????????? H);
- nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq ??));
- nchange with ((forall_memory_ranged ?????? ⊗ true) =true);
+ nrewrite > (anystatus_destruct_2 … H);
+ nrewrite > (anystatus_destruct_3 … H);
+ nrewrite > (anystatus_destruct_4 … H);
+ nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq …));
+ nchange with ((forall_memory_ranged … ⊗ true) =true);
  nrewrite > (symmetric_andbool (forall_memory_ranged t y3 y3 y2 y2 addrl) true);
- nchange with (forall_memory_ranged ?????? = true);
- napply (list_ind word16 ??? addrl);
- ##[ ##1,3,5,7: nnormalize; napply (refl_eq ??)
+ nchange with ((forall_memory_ranged t y3 y3 y2 y2 ?) = true);
+ napply (list_ind word16 … addrl);
+ ##[ ##1,3,5,7: nnormalize; napply refl_eq
  ##| ##2,4,6,8: #a; #l'; #H;
           nchange with (
           ((eq_option byte8 (mem_read t y2 y3 a)
                             (mem_read t y2 y3 a) eq_b8) ⊗
            (forall_memory_ranged t y3 y3 y2 y2 l')) = true);
           nrewrite > H;
-          nrewrite > (eq_to_eqoption ? (mem_read t y2 y3 a) (mem_read t y2 y3 a) eq_b8 eq_to_eqb8 (refl_eq ??));
+          nrewrite > (eq_to_eqoption ? (mem_read t y2 y3 a) (mem_read t y2 y3 a) eq_b8 eq_to_eqb8 (refl_eq …));
           nnormalize;
-          napply (refl_eq ??)
+          napply refl_eq
  ##]
 nqed.
 
@@ -1021,25 +1021,25 @@ nlemma eq_to_eqstatus_weak :
           nchange with (((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
           nchange in H:(%) with (x1 = y1);
           nrewrite > H; 
-          nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq ??))
+          nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq …))
  ##| ##2,3: #s1; ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
           nchange with (((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
           nchange in H:(%) with (x1 = y1);
           nrewrite > H; 
-          nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq ??))
+          nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq …))
  ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4;
           #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
           nchange with (((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
           nchange in H:(%) with (x1 = y1);
           nrewrite > H; 
-          nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq ??))
+          nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq …))
  ##]
  nchange in H2:(%) with (forall_memory_ranged t x3 y3 x2 y2 addrl = true);
  nrewrite > H2;
  nchange in H1:(%) with (x4 = y4);
  nrewrite > H1;
- nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq ??));
+ nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq …));
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.