factorized common components of objects

[helm.git] / helm / software / matita / library / freescale / exadecim.ma

diff --git a/helm/software/matita/library/freescale/exadecim.ma b/helm/software/matita/library/freescale/exadecim.ma
index 21a31c98e0c64fc595025858a9e068a2a8a50fec..f7afbdf6c3cda3590eff2a050c37f5f7e2d3b166 100644 (file)
--- a/helm/software/matita/library/freescale/exadecim.ma
+++ b/helm/software/matita/library/freescale/exadecim.ma
@@ -740,36 +740,36 @@ definition xor_ex ≝
 definition rcr_ex ≝
 λe:exadecim.λc:bool.match c with
  [ true ⇒ match e with
-  [ x0 ⇒ pairT exadecim bool x8 false | x1 ⇒ pairT exadecim bool x8 true
-  | x2 ⇒ pairT exadecim bool x9 false | x3 ⇒ pairT exadecim bool x9 true
-  | x4 ⇒ pairT exadecim bool xA false | x5 ⇒ pairT exadecim bool xA true
-  | x6 ⇒ pairT exadecim bool xB false | x7 ⇒ pairT exadecim bool xB true
-  | x8 ⇒ pairT exadecim bool xC false | x9 ⇒ pairT exadecim bool xC true
-  | xA ⇒ pairT exadecim bool xD false | xB ⇒ pairT exadecim bool xD true
-  | xC ⇒ pairT exadecim bool xE false | xD ⇒ pairT exadecim bool xE true
-  | xE ⇒ pairT exadecim bool xF false | xF ⇒ pairT exadecim bool xF true ]
+  [ x0 ⇒ pair exadecim bool x8 false | x1 ⇒ pair exadecim bool x8 true
+  | x2 ⇒ pair exadecim bool x9 false | x3 ⇒ pair exadecim bool x9 true
+  | x4 ⇒ pair exadecim bool xA false | x5 ⇒ pair exadecim bool xA true
+  | x6 ⇒ pair exadecim bool xB false | x7 ⇒ pair exadecim bool xB true
+  | x8 ⇒ pair exadecim bool xC false | x9 ⇒ pair exadecim bool xC true
+  | xA ⇒ pair exadecim bool xD false | xB ⇒ pair exadecim bool xD true
+  | xC ⇒ pair exadecim bool xE false | xD ⇒ pair exadecim bool xE true
+  | xE ⇒ pair exadecim bool xF false | xF ⇒ pair exadecim bool xF true ]
  | false ⇒ match e with 
-  [ x0 ⇒ pairT exadecim bool x0 false | x1 ⇒ pairT exadecim bool x0 true
-  | x2 ⇒ pairT exadecim bool x1 false | x3 ⇒ pairT exadecim bool x1 true
-  | x4 ⇒ pairT exadecim bool x2 false | x5 ⇒ pairT exadecim bool x2 true
-  | x6 ⇒ pairT exadecim bool x3 false | x7 ⇒ pairT exadecim bool x3 true
-  | x8 ⇒ pairT exadecim bool x4 false | x9 ⇒ pairT exadecim bool x4 true
-  | xA ⇒ pairT exadecim bool x5 false | xB ⇒ pairT exadecim bool x5 true
-  | xC ⇒ pairT exadecim bool x6 false | xD ⇒ pairT exadecim bool x6 true
-  | xE ⇒ pairT exadecim bool x7 false | xF ⇒ pairT exadecim bool x7 true ]
+  [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
+  | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
+  | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
+  | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
+  | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
+  | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
+  | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
+  | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ]
  ].
 
 (* operatore shift destro *)
 definition shr_ex ≝
 λe:exadecim.match e with 
- [ x0 ⇒ pairT exadecim bool x0 false | x1 ⇒ pairT exadecim bool x0 true
- | x2 ⇒ pairT exadecim bool x1 false | x3 ⇒ pairT exadecim bool x1 true
- | x4 ⇒ pairT exadecim bool x2 false | x5 ⇒ pairT exadecim bool x2 true
- | x6 ⇒ pairT exadecim bool x3 false | x7 ⇒ pairT exadecim bool x3 true
- | x8 ⇒ pairT exadecim bool x4 false | x9 ⇒ pairT exadecim bool x4 true
- | xA ⇒ pairT exadecim bool x5 false | xB ⇒ pairT exadecim bool x5 true
- | xC ⇒ pairT exadecim bool x6 false | xD ⇒ pairT exadecim bool x6 true
- | xE ⇒ pairT exadecim bool x7 false | xF ⇒ pairT exadecim bool x7 true ].
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x0 true
+ | x2 ⇒ pair exadecim bool x1 false | x3 ⇒ pair exadecim bool x1 true
+ | x4 ⇒ pair exadecim bool x2 false | x5 ⇒ pair exadecim bool x2 true
+ | x6 ⇒ pair exadecim bool x3 false | x7 ⇒ pair exadecim bool x3 true
+ | x8 ⇒ pair exadecim bool x4 false | x9 ⇒ pair exadecim bool x4 true
+ | xA ⇒ pair exadecim bool x5 false | xB ⇒ pair exadecim bool x5 true
+ | xC ⇒ pair exadecim bool x6 false | xD ⇒ pair exadecim bool x6 true
+ | xE ⇒ pair exadecim bool x7 false | xF ⇒ pair exadecim bool x7 true ].
 
 (* operatore rotazione destra *)
 definition ror_ex ≝
@@ -789,36 +789,36 @@ let rec ror_ex_n (e:exadecim) (n:nat) on n ≝
 definition rcl_ex ≝
 λe:exadecim.λc:bool.match c with
  [ true ⇒ match e with
-  [ x0 ⇒ pairT exadecim bool x1 false | x1 ⇒ pairT exadecim bool x3 false
-  | x2 ⇒ pairT exadecim bool x5 false | x3 ⇒ pairT exadecim bool x7 false
-  | x4 ⇒ pairT exadecim bool x9 false | x5 ⇒ pairT exadecim bool xB false
-  | x6 ⇒ pairT exadecim bool xD false | x7 ⇒ pairT exadecim bool xF false
-  | x8 ⇒ pairT exadecim bool x1 true  | x9 ⇒ pairT exadecim bool x3 true
-  | xA ⇒ pairT exadecim bool x5 true  | xB ⇒ pairT exadecim bool x7 true
-  | xC ⇒ pairT exadecim bool x9 true  | xD ⇒ pairT exadecim bool xB true
-  | xE ⇒ pairT exadecim bool xD true  | xF ⇒ pairT exadecim bool xF true ]
+  [ x0 ⇒ pair exadecim bool x1 false | x1 ⇒ pair exadecim bool x3 false
+  | x2 ⇒ pair exadecim bool x5 false | x3 ⇒ pair exadecim bool x7 false
+  | x4 ⇒ pair exadecim bool x9 false | x5 ⇒ pair exadecim bool xB false
+  | x6 ⇒ pair exadecim bool xD false | x7 ⇒ pair exadecim bool xF false
+  | x8 ⇒ pair exadecim bool x1 true  | x9 ⇒ pair exadecim bool x3 true
+  | xA ⇒ pair exadecim bool x5 true  | xB ⇒ pair exadecim bool x7 true
+  | xC ⇒ pair exadecim bool x9 true  | xD ⇒ pair exadecim bool xB true
+  | xE ⇒ pair exadecim bool xD true  | xF ⇒ pair exadecim bool xF true ]
  | false ⇒ match e with
-  [ x0 ⇒ pairT exadecim bool x0 false | x1 ⇒ pairT exadecim bool x2 false
-  | x2 ⇒ pairT exadecim bool x4 false | x3 ⇒ pairT exadecim bool x6 false
-  | x4 ⇒ pairT exadecim bool x8 false | x5 ⇒ pairT exadecim bool xA false
-  | x6 ⇒ pairT exadecim bool xC false | x7 ⇒ pairT exadecim bool xE false
-  | x8 ⇒ pairT exadecim bool x0 true  | x9 ⇒ pairT exadecim bool x2 true
-  | xA ⇒ pairT exadecim bool x4 true  | xB ⇒ pairT exadecim bool x6 true
-  | xC ⇒ pairT exadecim bool x8 true  | xD ⇒ pairT exadecim bool xA true
-  | xE ⇒ pairT exadecim bool xC true  | xF ⇒ pairT exadecim bool xE true ]
+  [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
+  | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
+  | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
+  | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
+  | x8 ⇒ pair exadecim bool x0 true  | x9 ⇒ pair exadecim bool x2 true
+  | xA ⇒ pair exadecim bool x4 true  | xB ⇒ pair exadecim bool x6 true
+  | xC ⇒ pair exadecim bool x8 true  | xD ⇒ pair exadecim bool xA true
+  | xE ⇒ pair exadecim bool xC true  | xF ⇒ pair exadecim bool xE true ]
  ].
 
 (* operatore shift sinistro *)
 definition shl_ex ≝
 λe:exadecim.match e with
- [ x0 ⇒ pairT exadecim bool x0 false | x1 ⇒ pairT exadecim bool x2 false
- | x2 ⇒ pairT exadecim bool x4 false | x3 ⇒ pairT exadecim bool x6 false
- | x4 ⇒ pairT exadecim bool x8 false | x5 ⇒ pairT exadecim bool xA false
- | x6 ⇒ pairT exadecim bool xC false | x7 ⇒ pairT exadecim bool xE false
- | x8 ⇒ pairT exadecim bool x0 true  | x9 ⇒ pairT exadecim bool x2 true
- | xA ⇒ pairT exadecim bool x4 true  | xB ⇒ pairT exadecim bool x6 true
- | xC ⇒ pairT exadecim bool x8 true  | xD ⇒ pairT exadecim bool xA true
- | xE ⇒ pairT exadecim bool xC true  | xF ⇒ pairT exadecim bool xE true ].
+ [ x0 ⇒ pair exadecim bool x0 false | x1 ⇒ pair exadecim bool x2 false
+ | x2 ⇒ pair exadecim bool x4 false | x3 ⇒ pair exadecim bool x6 false
+ | x4 ⇒ pair exadecim bool x8 false | x5 ⇒ pair exadecim bool xA false
+ | x6 ⇒ pair exadecim bool xC false | x7 ⇒ pair exadecim bool xE false
+ | x8 ⇒ pair exadecim bool x0 true  | x9 ⇒ pair exadecim bool x2 true
+ | xA ⇒ pair exadecim bool x4 true  | xB ⇒ pair exadecim bool x6 true
+ | xC ⇒ pair exadecim bool x8 true  | xD ⇒ pair exadecim bool xA true
+ | xE ⇒ pair exadecim bool xC true  | xF ⇒ pair exadecim bool xE true ].
 
 (* operatore rotazione sinistra *)
 definition rol_ex ≝
@@ -850,593 +850,593 @@ definition plus_ex ≝
       match e1 with
        [ x0 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x1 false
-            | x1 ⇒ pairT exadecim bool x2 false
-            | x2 ⇒ pairT exadecim bool x3 false
-            | x3 ⇒ pairT exadecim bool x4 false
-            | x4 ⇒ pairT exadecim bool x5 false
-            | x5 ⇒ pairT exadecim bool x6 false
-            | x6 ⇒ pairT exadecim bool x7 false
-            | x7 ⇒ pairT exadecim bool x8 false
-            | x8 ⇒ pairT exadecim bool x9 false
-            | x9 ⇒ pairT exadecim bool xA false
-            | xA ⇒ pairT exadecim bool xB false
-            | xB ⇒ pairT exadecim bool xC false
-            | xC ⇒ pairT exadecim bool xD false
-            | xD ⇒ pairT exadecim bool xE false
-            | xE ⇒ pairT exadecim bool xF false
-            | xF ⇒ pairT exadecim bool x0 true ] 
+            [ x0 ⇒ pair exadecim bool x1 false
+            | x1 ⇒ pair exadecim bool x2 false
+            | x2 ⇒ pair exadecim bool x3 false
+            | x3 ⇒ pair exadecim bool x4 false
+            | x4 ⇒ pair exadecim bool x5 false
+            | x5 ⇒ pair exadecim bool x6 false
+            | x6 ⇒ pair exadecim bool x7 false
+            | x7 ⇒ pair exadecim bool x8 false
+            | x8 ⇒ pair exadecim bool x9 false
+            | x9 ⇒ pair exadecim bool xA false
+            | xA ⇒ pair exadecim bool xB false
+            | xB ⇒ pair exadecim bool xC false
+            | xC ⇒ pair exadecim bool xD false
+            | xD ⇒ pair exadecim bool xE false
+            | xE ⇒ pair exadecim bool xF false
+            | xF ⇒ pair exadecim bool x0 true ] 
        | x1 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x2 false
-            | x1 ⇒ pairT exadecim bool x3 false
-            | x2 ⇒ pairT exadecim bool x4 false
-            | x3 ⇒ pairT exadecim bool x5 false
-            | x4 ⇒ pairT exadecim bool x6 false
-            | x5 ⇒ pairT exadecim bool x7 false
-            | x6 ⇒ pairT exadecim bool x8 false
-            | x7 ⇒ pairT exadecim bool x9 false
-            | x8 ⇒ pairT exadecim bool xA false
-            | x9 ⇒ pairT exadecim bool xB false
-            | xA ⇒ pairT exadecim bool xC false
-            | xB ⇒ pairT exadecim bool xD false
-            | xC ⇒ pairT exadecim bool xE false
-            | xD ⇒ pairT exadecim bool xF false
-            | xE ⇒ pairT exadecim bool x0 true
-            | xF ⇒ pairT exadecim bool x1 true ] 
+            [ x0 ⇒ pair exadecim bool x2 false
+            | x1 ⇒ pair exadecim bool x3 false
+            | x2 ⇒ pair exadecim bool x4 false
+            | x3 ⇒ pair exadecim bool x5 false
+            | x4 ⇒ pair exadecim bool x6 false
+            | x5 ⇒ pair exadecim bool x7 false
+            | x6 ⇒ pair exadecim bool x8 false
+            | x7 ⇒ pair exadecim bool x9 false
+            | x8 ⇒ pair exadecim bool xA false
+            | x9 ⇒ pair exadecim bool xB false
+            | xA ⇒ pair exadecim bool xC false
+            | xB ⇒ pair exadecim bool xD false
+            | xC ⇒ pair exadecim bool xE false
+            | xD ⇒ pair exadecim bool xF false
+            | xE ⇒ pair exadecim bool x0 true
+            | xF ⇒ pair exadecim bool x1 true ] 
        | x2 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x3 false
-            | x1 ⇒ pairT exadecim bool x4 false
-            | x2 ⇒ pairT exadecim bool x5 false
-            | x3 ⇒ pairT exadecim bool x6 false
-            | x4 ⇒ pairT exadecim bool x7 false
-            | x5 ⇒ pairT exadecim bool x8 false
-            | x6 ⇒ pairT exadecim bool x9 false
-            | x7 ⇒ pairT exadecim bool xA false
-            | x8 ⇒ pairT exadecim bool xB false
-            | x9 ⇒ pairT exadecim bool xC false
-            | xA ⇒ pairT exadecim bool xD false
-            | xB ⇒ pairT exadecim bool xE false
-            | xC ⇒ pairT exadecim bool xF false
-            | xD ⇒ pairT exadecim bool x0 true
-            | xE ⇒ pairT exadecim bool x1 true
-            | xF ⇒ pairT exadecim bool x2 true ] 
+            [ x0 ⇒ pair exadecim bool x3 false
+            | x1 ⇒ pair exadecim bool x4 false
+            | x2 ⇒ pair exadecim bool x5 false
+            | x3 ⇒ pair exadecim bool x6 false
+            | x4 ⇒ pair exadecim bool x7 false
+            | x5 ⇒ pair exadecim bool x8 false
+            | x6 ⇒ pair exadecim bool x9 false
+            | x7 ⇒ pair exadecim bool xA false
+            | x8 ⇒ pair exadecim bool xB false
+            | x9 ⇒ pair exadecim bool xC false
+            | xA ⇒ pair exadecim bool xD false
+            | xB ⇒ pair exadecim bool xE false
+            | xC ⇒ pair exadecim bool xF false
+            | xD ⇒ pair exadecim bool x0 true
+            | xE ⇒ pair exadecim bool x1 true
+            | xF ⇒ pair exadecim bool x2 true ] 
        | x3 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x4 false
-            | x1 ⇒ pairT exadecim bool x5 false
-            | x2 ⇒ pairT exadecim bool x6 false
-            | x3 ⇒ pairT exadecim bool x7 false
-            | x4 ⇒ pairT exadecim bool x8 false
-            | x5 ⇒ pairT exadecim bool x9 false
-            | x6 ⇒ pairT exadecim bool xA false
-            | x7 ⇒ pairT exadecim bool xB false
-            | x8 ⇒ pairT exadecim bool xC false
-            | x9 ⇒ pairT exadecim bool xD false
-            | xA ⇒ pairT exadecim bool xE false
-            | xB ⇒ pairT exadecim bool xF false
-            | xC ⇒ pairT exadecim bool x0 true
-            | xD ⇒ pairT exadecim bool x1 true
-            | xE ⇒ pairT exadecim bool x2 true
-            | xF ⇒ pairT exadecim bool x3 true ] 
+            [ x0 ⇒ pair exadecim bool x4 false
+            | x1 ⇒ pair exadecim bool x5 false
+            | x2 ⇒ pair exadecim bool x6 false
+            | x3 ⇒ pair exadecim bool x7 false
+            | x4 ⇒ pair exadecim bool x8 false
+            | x5 ⇒ pair exadecim bool x9 false
+            | x6 ⇒ pair exadecim bool xA false
+            | x7 ⇒ pair exadecim bool xB false
+            | x8 ⇒ pair exadecim bool xC false
+            | x9 ⇒ pair exadecim bool xD false
+            | xA ⇒ pair exadecim bool xE false
+            | xB ⇒ pair exadecim bool xF false
+            | xC ⇒ pair exadecim bool x0 true
+            | xD ⇒ pair exadecim bool x1 true
+            | xE ⇒ pair exadecim bool x2 true
+            | xF ⇒ pair exadecim bool x3 true ] 
        | x4 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x5 false
-            | x1 ⇒ pairT exadecim bool x6 false
-            | x2 ⇒ pairT exadecim bool x7 false
-            | x3 ⇒ pairT exadecim bool x8 false
-            | x4 ⇒ pairT exadecim bool x9 false
-            | x5 ⇒ pairT exadecim bool xA false
-            | x6 ⇒ pairT exadecim bool xB false
-            | x7 ⇒ pairT exadecim bool xC false
-            | x8 ⇒ pairT exadecim bool xD false
-            | x9 ⇒ pairT exadecim bool xE false
-            | xA ⇒ pairT exadecim bool xF false
-            | xB ⇒ pairT exadecim bool x0 true
-            | xC ⇒ pairT exadecim bool x1 true
-            | xD ⇒ pairT exadecim bool x2 true
-            | xE ⇒ pairT exadecim bool x3 true
-            | xF ⇒ pairT exadecim bool x4 true ] 
+            [ x0 ⇒ pair exadecim bool x5 false
+            | x1 ⇒ pair exadecim bool x6 false
+            | x2 ⇒ pair exadecim bool x7 false
+            | x3 ⇒ pair exadecim bool x8 false
+            | x4 ⇒ pair exadecim bool x9 false
+            | x5 ⇒ pair exadecim bool xA false
+            | x6 ⇒ pair exadecim bool xB false
+            | x7 ⇒ pair exadecim bool xC false
+            | x8 ⇒ pair exadecim bool xD false
+            | x9 ⇒ pair exadecim bool xE false
+            | xA ⇒ pair exadecim bool xF false
+            | xB ⇒ pair exadecim bool x0 true
+            | xC ⇒ pair exadecim bool x1 true
+            | xD ⇒ pair exadecim bool x2 true
+            | xE ⇒ pair exadecim bool x3 true
+            | xF ⇒ pair exadecim bool x4 true ] 
        | x5 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x6 false
-            | x1 ⇒ pairT exadecim bool x7 false
-            | x2 ⇒ pairT exadecim bool x8 false
-            | x3 ⇒ pairT exadecim bool x9 false
-            | x4 ⇒ pairT exadecim bool xA false
-            | x5 ⇒ pairT exadecim bool xB false
-            | x6 ⇒ pairT exadecim bool xC false
-            | x7 ⇒ pairT exadecim bool xD false
-            | x8 ⇒ pairT exadecim bool xE false
-            | x9 ⇒ pairT exadecim bool xF false
-            | xA ⇒ pairT exadecim bool x0 true
-            | xB ⇒ pairT exadecim bool x1 true
-            | xC ⇒ pairT exadecim bool x2 true
-            | xD ⇒ pairT exadecim bool x3 true
-            | xE ⇒ pairT exadecim bool x4 true
-            | xF ⇒ pairT exadecim bool x5 true ] 
+            [ x0 ⇒ pair exadecim bool x6 false
+            | x1 ⇒ pair exadecim bool x7 false
+            | x2 ⇒ pair exadecim bool x8 false
+            | x3 ⇒ pair exadecim bool x9 false
+            | x4 ⇒ pair exadecim bool xA false
+            | x5 ⇒ pair exadecim bool xB false
+            | x6 ⇒ pair exadecim bool xC false
+            | x7 ⇒ pair exadecim bool xD false
+            | x8 ⇒ pair exadecim bool xE false
+            | x9 ⇒ pair exadecim bool xF false
+            | xA ⇒ pair exadecim bool x0 true
+            | xB ⇒ pair exadecim bool x1 true
+            | xC ⇒ pair exadecim bool x2 true
+            | xD ⇒ pair exadecim bool x3 true
+            | xE ⇒ pair exadecim bool x4 true
+            | xF ⇒ pair exadecim bool x5 true ] 
        | x6 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x7 false
-            | x1 ⇒ pairT exadecim bool x8 false
-            | x2 ⇒ pairT exadecim bool x9 false
-            | x3 ⇒ pairT exadecim bool xA false
-            | x4 ⇒ pairT exadecim bool xB false
-            | x5 ⇒ pairT exadecim bool xC false
-            | x6 ⇒ pairT exadecim bool xD false
-            | x7 ⇒ pairT exadecim bool xE false
-            | x8 ⇒ pairT exadecim bool xF false
-            | x9 ⇒ pairT exadecim bool x0 true
-            | xA ⇒ pairT exadecim bool x1 true
-            | xB ⇒ pairT exadecim bool x2 true
-            | xC ⇒ pairT exadecim bool x3 true
-            | xD ⇒ pairT exadecim bool x4 true
-            | xE ⇒ pairT exadecim bool x5 true
-            | xF ⇒ pairT exadecim bool x6 true ] 
+            [ x0 ⇒ pair exadecim bool x7 false
+            | x1 ⇒ pair exadecim bool x8 false
+            | x2 ⇒ pair exadecim bool x9 false
+            | x3 ⇒ pair exadecim bool xA false
+            | x4 ⇒ pair exadecim bool xB false
+            | x5 ⇒ pair exadecim bool xC false
+            | x6 ⇒ pair exadecim bool xD false
+            | x7 ⇒ pair exadecim bool xE false
+            | x8 ⇒ pair exadecim bool xF false
+            | x9 ⇒ pair exadecim bool x0 true
+            | xA ⇒ pair exadecim bool x1 true
+            | xB ⇒ pair exadecim bool x2 true
+            | xC ⇒ pair exadecim bool x3 true
+            | xD ⇒ pair exadecim bool x4 true
+            | xE ⇒ pair exadecim bool x5 true
+            | xF ⇒ pair exadecim bool x6 true ] 
        | x7 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x8 false
-            | x1 ⇒ pairT exadecim bool x9 false
-            | x2 ⇒ pairT exadecim bool xA false
-            | x3 ⇒ pairT exadecim bool xB false
-            | x4 ⇒ pairT exadecim bool xC false
-            | x5 ⇒ pairT exadecim bool xD false
-            | x6 ⇒ pairT exadecim bool xE false
-            | x7 ⇒ pairT exadecim bool xF false
-            | x8 ⇒ pairT exadecim bool x0 true
-            | x9 ⇒ pairT exadecim bool x1 true
-            | xA ⇒ pairT exadecim bool x2 true
-            | xB ⇒ pairT exadecim bool x3 true
-            | xC ⇒ pairT exadecim bool x4 true
-            | xD ⇒ pairT exadecim bool x5 true
-            | xE ⇒ pairT exadecim bool x6 true
-            | xF ⇒ pairT exadecim bool x7 true ] 
+            [ x0 ⇒ pair exadecim bool x8 false
+            | x1 ⇒ pair exadecim bool x9 false
+            | x2 ⇒ pair exadecim bool xA false
+            | x3 ⇒ pair exadecim bool xB false
+            | x4 ⇒ pair exadecim bool xC false
+            | x5 ⇒ pair exadecim bool xD false
+            | x6 ⇒ pair exadecim bool xE false
+            | x7 ⇒ pair exadecim bool xF false
+            | x8 ⇒ pair exadecim bool x0 true
+            | x9 ⇒ pair exadecim bool x1 true
+            | xA ⇒ pair exadecim bool x2 true
+            | xB ⇒ pair exadecim bool x3 true
+            | xC ⇒ pair exadecim bool x4 true
+            | xD ⇒ pair exadecim bool x5 true
+            | xE ⇒ pair exadecim bool x6 true
+            | xF ⇒ pair exadecim bool x7 true ] 
        | x8 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x9 false
-            | x1 ⇒ pairT exadecim bool xA false
-            | x2 ⇒ pairT exadecim bool xB false
-            | x3 ⇒ pairT exadecim bool xC false
-            | x4 ⇒ pairT exadecim bool xD false
-            | x5 ⇒ pairT exadecim bool xE false
-            | x6 ⇒ pairT exadecim bool xF false
-            | x7 ⇒ pairT exadecim bool x0 true
-            | x8 ⇒ pairT exadecim bool x1 true
-            | x9 ⇒ pairT exadecim bool x2 true
-            | xA ⇒ pairT exadecim bool x3 true
-            | xB ⇒ pairT exadecim bool x4 true
-            | xC ⇒ pairT exadecim bool x5 true
-            | xD ⇒ pairT exadecim bool x6 true
-            | xE ⇒ pairT exadecim bool x7 true
-            | xF ⇒ pairT exadecim bool x8 true ] 
+            [ x0 ⇒ pair exadecim bool x9 false
+            | x1 ⇒ pair exadecim bool xA false
+            | x2 ⇒ pair exadecim bool xB false
+            | x3 ⇒ pair exadecim bool xC false
+            | x4 ⇒ pair exadecim bool xD false
+            | x5 ⇒ pair exadecim bool xE false
+            | x6 ⇒ pair exadecim bool xF false
+            | x7 ⇒ pair exadecim bool x0 true
+            | x8 ⇒ pair exadecim bool x1 true
+            | x9 ⇒ pair exadecim bool x2 true
+            | xA ⇒ pair exadecim bool x3 true
+            | xB ⇒ pair exadecim bool x4 true
+            | xC ⇒ pair exadecim bool x5 true
+            | xD ⇒ pair exadecim bool x6 true
+            | xE ⇒ pair exadecim bool x7 true
+            | xF ⇒ pair exadecim bool x8 true ] 
        | x9 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool xA false
-            | x1 ⇒ pairT exadecim bool xB false
-            | x2 ⇒ pairT exadecim bool xC false
-            | x3 ⇒ pairT exadecim bool xD false
-            | x4 ⇒ pairT exadecim bool xE false
-            | x5 ⇒ pairT exadecim bool xF false
-            | x6 ⇒ pairT exadecim bool x0 true
-            | x7 ⇒ pairT exadecim bool x1 true
-            | x8 ⇒ pairT exadecim bool x2 true
-            | x9 ⇒ pairT exadecim bool x3 true
-            | xA ⇒ pairT exadecim bool x4 true
-            | xB ⇒ pairT exadecim bool x5 true
-            | xC ⇒ pairT exadecim bool x6 true
-            | xD ⇒ pairT exadecim bool x7 true
-            | xE ⇒ pairT exadecim bool x8 true
-            | xF ⇒ pairT exadecim bool x9 true ] 
+            [ x0 ⇒ pair exadecim bool xA false
+            | x1 ⇒ pair exadecim bool xB false
+            | x2 ⇒ pair exadecim bool xC false
+            | x3 ⇒ pair exadecim bool xD false
+            | x4 ⇒ pair exadecim bool xE false
+            | x5 ⇒ pair exadecim bool xF false
+            | x6 ⇒ pair exadecim bool x0 true
+            | x7 ⇒ pair exadecim bool x1 true
+            | x8 ⇒ pair exadecim bool x2 true
+            | x9 ⇒ pair exadecim bool x3 true
+            | xA ⇒ pair exadecim bool x4 true
+            | xB ⇒ pair exadecim bool x5 true
+            | xC ⇒ pair exadecim bool x6 true
+            | xD ⇒ pair exadecim bool x7 true
+            | xE ⇒ pair exadecim bool x8 true
+            | xF ⇒ pair exadecim bool x9 true ] 
        | xA ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool xB false
-            | x1 ⇒ pairT exadecim bool xC false
-            | x2 ⇒ pairT exadecim bool xD false
-            | x3 ⇒ pairT exadecim bool xE false
-            | x4 ⇒ pairT exadecim bool xF false
-            | x5 ⇒ pairT exadecim bool x0 true
-            | x6 ⇒ pairT exadecim bool x1 true
-            | x7 ⇒ pairT exadecim bool x2 true
-            | x8 ⇒ pairT exadecim bool x3 true
-            | x9 ⇒ pairT exadecim bool x4 true
-            | xA ⇒ pairT exadecim bool x5 true
-            | xB ⇒ pairT exadecim bool x6 true
-            | xC ⇒ pairT exadecim bool x7 true
-            | xD ⇒ pairT exadecim bool x8 true
-            | xE ⇒ pairT exadecim bool x9 true
-            | xF ⇒ pairT exadecim bool xA true ] 
+            [ x0 ⇒ pair exadecim bool xB false
+            | x1 ⇒ pair exadecim bool xC false
+            | x2 ⇒ pair exadecim bool xD false
+            | x3 ⇒ pair exadecim bool xE false
+            | x4 ⇒ pair exadecim bool xF false
+            | x5 ⇒ pair exadecim bool x0 true
+            | x6 ⇒ pair exadecim bool x1 true
+            | x7 ⇒ pair exadecim bool x2 true
+            | x8 ⇒ pair exadecim bool x3 true
+            | x9 ⇒ pair exadecim bool x4 true
+            | xA ⇒ pair exadecim bool x5 true
+            | xB ⇒ pair exadecim bool x6 true
+            | xC ⇒ pair exadecim bool x7 true
+            | xD ⇒ pair exadecim bool x8 true
+            | xE ⇒ pair exadecim bool x9 true
+            | xF ⇒ pair exadecim bool xA true ] 
        | xB ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool xC false
-            | x1 ⇒ pairT exadecim bool xD false
-            | x2 ⇒ pairT exadecim bool xE false
-            | x3 ⇒ pairT exadecim bool xF false
-            | x4 ⇒ pairT exadecim bool x0 true
-            | x5 ⇒ pairT exadecim bool x1 true
-            | x6 ⇒ pairT exadecim bool x2 true
-            | x7 ⇒ pairT exadecim bool x3 true
-            | x8 ⇒ pairT exadecim bool x4 true
-            | x9 ⇒ pairT exadecim bool x5 true
-            | xA ⇒ pairT exadecim bool x6 true
-            | xB ⇒ pairT exadecim bool x7 true
-            | xC ⇒ pairT exadecim bool x8 true
-            | xD ⇒ pairT exadecim bool x9 true
-            | xE ⇒ pairT exadecim bool xA true
-            | xF ⇒ pairT exadecim bool xB true ] 
+            [ x0 ⇒ pair exadecim bool xC false
+            | x1 ⇒ pair exadecim bool xD false
+            | x2 ⇒ pair exadecim bool xE false
+            | x3 ⇒ pair exadecim bool xF false
+            | x4 ⇒ pair exadecim bool x0 true
+            | x5 ⇒ pair exadecim bool x1 true
+            | x6 ⇒ pair exadecim bool x2 true
+            | x7 ⇒ pair exadecim bool x3 true
+            | x8 ⇒ pair exadecim bool x4 true
+            | x9 ⇒ pair exadecim bool x5 true
+            | xA ⇒ pair exadecim bool x6 true
+            | xB ⇒ pair exadecim bool x7 true
+            | xC ⇒ pair exadecim bool x8 true
+            | xD ⇒ pair exadecim bool x9 true
+            | xE ⇒ pair exadecim bool xA true
+            | xF ⇒ pair exadecim bool xB true ] 
        | xC ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool xD false
-            | x1 ⇒ pairT exadecim bool xE false
-            | x2 ⇒ pairT exadecim bool xF false
-            | x3 ⇒ pairT exadecim bool x0 true
-            | x4 ⇒ pairT exadecim bool x1 true
-            | x5 ⇒ pairT exadecim bool x2 true
-            | x6 ⇒ pairT exadecim bool x3 true
-            | x7 ⇒ pairT exadecim bool x4 true
-            | x8 ⇒ pairT exadecim bool x5 true
-            | x9 ⇒ pairT exadecim bool x6 true
-            | xA ⇒ pairT exadecim bool x7 true
-            | xB ⇒ pairT exadecim bool x8 true
-            | xC ⇒ pairT exadecim bool x9 true
-            | xD ⇒ pairT exadecim bool xA true
-            | xE ⇒ pairT exadecim bool xB true
-            | xF ⇒ pairT exadecim bool xC true ] 
+            [ x0 ⇒ pair exadecim bool xD false
+            | x1 ⇒ pair exadecim bool xE false
+            | x2 ⇒ pair exadecim bool xF false
+            | x3 ⇒ pair exadecim bool x0 true
+            | x4 ⇒ pair exadecim bool x1 true
+            | x5 ⇒ pair exadecim bool x2 true
+            | x6 ⇒ pair exadecim bool x3 true
+            | x7 ⇒ pair exadecim bool x4 true
+            | x8 ⇒ pair exadecim bool x5 true
+            | x9 ⇒ pair exadecim bool x6 true
+            | xA ⇒ pair exadecim bool x7 true
+            | xB ⇒ pair exadecim bool x8 true
+            | xC ⇒ pair exadecim bool x9 true
+            | xD ⇒ pair exadecim bool xA true
+            | xE ⇒ pair exadecim bool xB true
+            | xF ⇒ pair exadecim bool xC true ] 
        | xD ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool xE false
-            | x1 ⇒ pairT exadecim bool xF false
-            | x2 ⇒ pairT exadecim bool x0 true
-            | x3 ⇒ pairT exadecim bool x1 true
-            | x4 ⇒ pairT exadecim bool x2 true
-            | x5 ⇒ pairT exadecim bool x3 true
-            | x6 ⇒ pairT exadecim bool x4 true
-            | x7 ⇒ pairT exadecim bool x5 true
-            | x8 ⇒ pairT exadecim bool x6 true
-            | x9 ⇒ pairT exadecim bool x7 true
-            | xA ⇒ pairT exadecim bool x8 true
-            | xB ⇒ pairT exadecim bool x9 true
-            | xC ⇒ pairT exadecim bool xA true
-            | xD ⇒ pairT exadecim bool xB true
-            | xE ⇒ pairT exadecim bool xC true
-            | xF ⇒ pairT exadecim bool xD true ] 
+            [ x0 ⇒ pair exadecim bool xE false
+            | x1 ⇒ pair exadecim bool xF false
+            | x2 ⇒ pair exadecim bool x0 true
+            | x3 ⇒ pair exadecim bool x1 true
+            | x4 ⇒ pair exadecim bool x2 true
+            | x5 ⇒ pair exadecim bool x3 true
+            | x6 ⇒ pair exadecim bool x4 true
+            | x7 ⇒ pair exadecim bool x5 true
+            | x8 ⇒ pair exadecim bool x6 true
+            | x9 ⇒ pair exadecim bool x7 true
+            | xA ⇒ pair exadecim bool x8 true
+            | xB ⇒ pair exadecim bool x9 true
+            | xC ⇒ pair exadecim bool xA true
+            | xD ⇒ pair exadecim bool xB true
+            | xE ⇒ pair exadecim bool xC true
+            | xF ⇒ pair exadecim bool xD true ] 
        | xE ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool xF false
-            | x1 ⇒ pairT exadecim bool x0 true
-            | x2 ⇒ pairT exadecim bool x1 true
-            | x3 ⇒ pairT exadecim bool x2 true
-            | x4 ⇒ pairT exadecim bool x3 true
-            | x5 ⇒ pairT exadecim bool x4 true
-            | x6 ⇒ pairT exadecim bool x5 true
-            | x7 ⇒ pairT exadecim bool x6 true
-            | x8 ⇒ pairT exadecim bool x7 true
-            | x9 ⇒ pairT exadecim bool x8 true
-            | xA ⇒ pairT exadecim bool x9 true
-            | xB ⇒ pairT exadecim bool xA true
-            | xC ⇒ pairT exadecim bool xB true
-            | xD ⇒ pairT exadecim bool xC true
-            | xE ⇒ pairT exadecim bool xD true
-            | xF ⇒ pairT exadecim bool xE true ]
+            [ x0 ⇒ pair exadecim bool xF false
+            | x1 ⇒ pair exadecim bool x0 true
+            | x2 ⇒ pair exadecim bool x1 true
+            | x3 ⇒ pair exadecim bool x2 true
+            | x4 ⇒ pair exadecim bool x3 true
+            | x5 ⇒ pair exadecim bool x4 true
+            | x6 ⇒ pair exadecim bool x5 true
+            | x7 ⇒ pair exadecim bool x6 true
+            | x8 ⇒ pair exadecim bool x7 true
+            | x9 ⇒ pair exadecim bool x8 true
+            | xA ⇒ pair exadecim bool x9 true
+            | xB ⇒ pair exadecim bool xA true
+            | xC ⇒ pair exadecim bool xB true
+            | xD ⇒ pair exadecim bool xC true
+            | xE ⇒ pair exadecim bool xD true
+            | xF ⇒ pair exadecim bool xE true ]
        | xF ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x0 true
-            | x1 ⇒ pairT exadecim bool x1 true
-            | x2 ⇒ pairT exadecim bool x2 true
-            | x3 ⇒ pairT exadecim bool x3 true
-            | x4 ⇒ pairT exadecim bool x4 true
-            | x5 ⇒ pairT exadecim bool x5 true
-            | x6 ⇒ pairT exadecim bool x6 true
-            | x7 ⇒ pairT exadecim bool x7 true
-            | x8 ⇒ pairT exadecim bool x8 true
-            | x9 ⇒ pairT exadecim bool x9 true
-            | xA ⇒ pairT exadecim bool xA true
-            | xB ⇒ pairT exadecim bool xB true
-            | xC ⇒ pairT exadecim bool xC true
-            | xD ⇒ pairT exadecim bool xD true
-            | xE ⇒ pairT exadecim bool xE true
-            | xF ⇒ pairT exadecim bool xF true ] 
+            [ x0 ⇒ pair exadecim bool x0 true
+            | x1 ⇒ pair exadecim bool x1 true
+            | x2 ⇒ pair exadecim bool x2 true
+            | x3 ⇒ pair exadecim bool x3 true
+            | x4 ⇒ pair exadecim bool x4 true
+            | x5 ⇒ pair exadecim bool x5 true
+            | x6 ⇒ pair exadecim bool x6 true
+            | x7 ⇒ pair exadecim bool x7 true
+            | x8 ⇒ pair exadecim bool x8 true
+            | x9 ⇒ pair exadecim bool x9 true
+            | xA ⇒ pair exadecim bool xA true
+            | xB ⇒ pair exadecim bool xB true
+            | xC ⇒ pair exadecim bool xC true
+            | xD ⇒ pair exadecim bool xD true
+            | xE ⇒ pair exadecim bool xE true
+            | xF ⇒ pair exadecim bool xF true ] 
        ]
    | false ⇒
       match e1 with
        [ x0 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x0 false
-            | x1 ⇒ pairT exadecim bool x1 false
-            | x2 ⇒ pairT exadecim bool x2 false
-            | x3 ⇒ pairT exadecim bool x3 false
-            | x4 ⇒ pairT exadecim bool x4 false
-            | x5 ⇒ pairT exadecim bool x5 false
-            | x6 ⇒ pairT exadecim bool x6 false
-            | x7 ⇒ pairT exadecim bool x7 false
-            | x8 ⇒ pairT exadecim bool x8 false
-            | x9 ⇒ pairT exadecim bool x9 false
-            | xA ⇒ pairT exadecim bool xA false
-            | xB ⇒ pairT exadecim bool xB false
-            | xC ⇒ pairT exadecim bool xC false
-            | xD ⇒ pairT exadecim bool xD false
-            | xE ⇒ pairT exadecim bool xE false
-            | xF ⇒ pairT exadecim bool xF false ] 
+            [ x0 ⇒ pair exadecim bool x0 false
+            | x1 ⇒ pair exadecim bool x1 false
+            | x2 ⇒ pair exadecim bool x2 false
+            | x3 ⇒ pair exadecim bool x3 false
+            | x4 ⇒ pair exadecim bool x4 false
+            | x5 ⇒ pair exadecim bool x5 false
+            | x6 ⇒ pair exadecim bool x6 false
+            | x7 ⇒ pair exadecim bool x7 false
+            | x8 ⇒ pair exadecim bool x8 false
+            | x9 ⇒ pair exadecim bool x9 false
+            | xA ⇒ pair exadecim bool xA false
+            | xB ⇒ pair exadecim bool xB false
+            | xC ⇒ pair exadecim bool xC false
+            | xD ⇒ pair exadecim bool xD false
+            | xE ⇒ pair exadecim bool xE false
+            | xF ⇒ pair exadecim bool xF false ] 
        | x1 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x1 false
-            | x1 ⇒ pairT exadecim bool x2 false
-            | x2 ⇒ pairT exadecim bool x3 false
-            | x3 ⇒ pairT exadecim bool x4 false
-            | x4 ⇒ pairT exadecim bool x5 false
-            | x5 ⇒ pairT exadecim bool x6 false
-            | x6 ⇒ pairT exadecim bool x7 false
-            | x7 ⇒ pairT exadecim bool x8 false
-            | x8 ⇒ pairT exadecim bool x9 false
-            | x9 ⇒ pairT exadecim bool xA false
-            | xA ⇒ pairT exadecim bool xB false
-            | xB ⇒ pairT exadecim bool xC false
-            | xC ⇒ pairT exadecim bool xD false
-            | xD ⇒ pairT exadecim bool xE false
-            | xE ⇒ pairT exadecim bool xF false
-            | xF ⇒ pairT exadecim bool x0 true ] 
+            [ x0 ⇒ pair exadecim bool x1 false
+            | x1 ⇒ pair exadecim bool x2 false
+            | x2 ⇒ pair exadecim bool x3 false
+            | x3 ⇒ pair exadecim bool x4 false
+            | x4 ⇒ pair exadecim bool x5 false
+            | x5 ⇒ pair exadecim bool x6 false
+            | x6 ⇒ pair exadecim bool x7 false
+            | x7 ⇒ pair exadecim bool x8 false
+            | x8 ⇒ pair exadecim bool x9 false
+            | x9 ⇒ pair exadecim bool xA false
+            | xA ⇒ pair exadecim bool xB false
+            | xB ⇒ pair exadecim bool xC false
+            | xC ⇒ pair exadecim bool xD false
+            | xD ⇒ pair exadecim bool xE false
+            | xE ⇒ pair exadecim bool xF false
+            | xF ⇒ pair exadecim bool x0 true ] 
        | x2 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x2 false
-            | x1 ⇒ pairT exadecim bool x3 false
-            | x2 ⇒ pairT exadecim bool x4 false
-            | x3 ⇒ pairT exadecim bool x5 false
-            | x4 ⇒ pairT exadecim bool x6 false
-            | x5 ⇒ pairT exadecim bool x7 false
-            | x6 ⇒ pairT exadecim bool x8 false
-            | x7 ⇒ pairT exadecim bool x9 false
-            | x8 ⇒ pairT exadecim bool xA false
-            | x9 ⇒ pairT exadecim bool xB false
-            | xA ⇒ pairT exadecim bool xC false
-            | xB ⇒ pairT exadecim bool xD false
-            | xC ⇒ pairT exadecim bool xE false
-            | xD ⇒ pairT exadecim bool xF false
-            | xE ⇒ pairT exadecim bool x0 true
-            | xF ⇒ pairT exadecim bool x1 true ] 
+            [ x0 ⇒ pair exadecim bool x2 false
+            | x1 ⇒ pair exadecim bool x3 false
+            | x2 ⇒ pair exadecim bool x4 false
+            | x3 ⇒ pair exadecim bool x5 false
+            | x4 ⇒ pair exadecim bool x6 false
+            | x5 ⇒ pair exadecim bool x7 false
+            | x6 ⇒ pair exadecim bool x8 false
+            | x7 ⇒ pair exadecim bool x9 false
+            | x8 ⇒ pair exadecim bool xA false
+            | x9 ⇒ pair exadecim bool xB false
+            | xA ⇒ pair exadecim bool xC false
+            | xB ⇒ pair exadecim bool xD false
+            | xC ⇒ pair exadecim bool xE false
+            | xD ⇒ pair exadecim bool xF false
+            | xE ⇒ pair exadecim bool x0 true
+            | xF ⇒ pair exadecim bool x1 true ] 
        | x3 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x3 false
-            | x1 ⇒ pairT exadecim bool x4 false
-            | x2 ⇒ pairT exadecim bool x5 false
-            | x3 ⇒ pairT exadecim bool x6 false
-            | x4 ⇒ pairT exadecim bool x7 false
-            | x5 ⇒ pairT exadecim bool x8 false
-            | x6 ⇒ pairT exadecim bool x9 false
-            | x7 ⇒ pairT exadecim bool xA false
-            | x8 ⇒ pairT exadecim bool xB false
-            | x9 ⇒ pairT exadecim bool xC false
-            | xA ⇒ pairT exadecim bool xD false
-            | xB ⇒ pairT exadecim bool xE false
-            | xC ⇒ pairT exadecim bool xF false
-            | xD ⇒ pairT exadecim bool x0 true
-            | xE ⇒ pairT exadecim bool x1 true
-            | xF ⇒ pairT exadecim bool x2 true ] 
+            [ x0 ⇒ pair exadecim bool x3 false
+            | x1 ⇒ pair exadecim bool x4 false
+            | x2 ⇒ pair exadecim bool x5 false
+            | x3 ⇒ pair exadecim bool x6 false
+            | x4 ⇒ pair exadecim bool x7 false
+            | x5 ⇒ pair exadecim bool x8 false
+            | x6 ⇒ pair exadecim bool x9 false
+            | x7 ⇒ pair exadecim bool xA false
+            | x8 ⇒ pair exadecim bool xB false
+            | x9 ⇒ pair exadecim bool xC false
+            | xA ⇒ pair exadecim bool xD false
+            | xB ⇒ pair exadecim bool xE false
+            | xC ⇒ pair exadecim bool xF false
+            | xD ⇒ pair exadecim bool x0 true
+            | xE ⇒ pair exadecim bool x1 true
+            | xF ⇒ pair exadecim bool x2 true ] 
        | x4 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x4 false
-            | x1 ⇒ pairT exadecim bool x5 false
-            | x2 ⇒ pairT exadecim bool x6 false
-            | x3 ⇒ pairT exadecim bool x7 false
-            | x4 ⇒ pairT exadecim bool x8 false
-            | x5 ⇒ pairT exadecim bool x9 false
-            | x6 ⇒ pairT exadecim bool xA false
-            | x7 ⇒ pairT exadecim bool xB false
-            | x8 ⇒ pairT exadecim bool xC false
-            | x9 ⇒ pairT exadecim bool xD false
-            | xA ⇒ pairT exadecim bool xE false
-            | xB ⇒ pairT exadecim bool xF false
-            | xC ⇒ pairT exadecim bool x0 true
-            | xD ⇒ pairT exadecim bool x1 true
-            | xE ⇒ pairT exadecim bool x2 true
-            | xF ⇒ pairT exadecim bool x3 true ] 
+            [ x0 ⇒ pair exadecim bool x4 false
+            | x1 ⇒ pair exadecim bool x5 false
+            | x2 ⇒ pair exadecim bool x6 false
+            | x3 ⇒ pair exadecim bool x7 false
+            | x4 ⇒ pair exadecim bool x8 false
+            | x5 ⇒ pair exadecim bool x9 false
+            | x6 ⇒ pair exadecim bool xA false
+            | x7 ⇒ pair exadecim bool xB false
+            | x8 ⇒ pair exadecim bool xC false
+            | x9 ⇒ pair exadecim bool xD false
+            | xA ⇒ pair exadecim bool xE false
+            | xB ⇒ pair exadecim bool xF false
+            | xC ⇒ pair exadecim bool x0 true
+            | xD ⇒ pair exadecim bool x1 true
+            | xE ⇒ pair exadecim bool x2 true
+            | xF ⇒ pair exadecim bool x3 true ] 
        | x5 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x5 false
-            | x1 ⇒ pairT exadecim bool x6 false
-            | x2 ⇒ pairT exadecim bool x7 false
-            | x3 ⇒ pairT exadecim bool x8 false
-            | x4 ⇒ pairT exadecim bool x9 false
-            | x5 ⇒ pairT exadecim bool xA false
-            | x6 ⇒ pairT exadecim bool xB false
-            | x7 ⇒ pairT exadecim bool xC false
-            | x8 ⇒ pairT exadecim bool xD false
-            | x9 ⇒ pairT exadecim bool xE false
-            | xA ⇒ pairT exadecim bool xF false
-            | xB ⇒ pairT exadecim bool x0 true
-            | xC ⇒ pairT exadecim bool x1 true
-            | xD ⇒ pairT exadecim bool x2 true
-            | xE ⇒ pairT exadecim bool x3 true
-            | xF ⇒ pairT exadecim bool x4 true ] 
+            [ x0 ⇒ pair exadecim bool x5 false
+            | x1 ⇒ pair exadecim bool x6 false
+            | x2 ⇒ pair exadecim bool x7 false
+            | x3 ⇒ pair exadecim bool x8 false
+            | x4 ⇒ pair exadecim bool x9 false
+            | x5 ⇒ pair exadecim bool xA false
+            | x6 ⇒ pair exadecim bool xB false
+            | x7 ⇒ pair exadecim bool xC false
+            | x8 ⇒ pair exadecim bool xD false
+            | x9 ⇒ pair exadecim bool xE false
+            | xA ⇒ pair exadecim bool xF false
+            | xB ⇒ pair exadecim bool x0 true
+            | xC ⇒ pair exadecim bool x1 true
+            | xD ⇒ pair exadecim bool x2 true
+            | xE ⇒ pair exadecim bool x3 true
+            | xF ⇒ pair exadecim bool x4 true ] 
        | x6 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x6 false
-            | x1 ⇒ pairT exadecim bool x7 false
-            | x2 ⇒ pairT exadecim bool x8 false
-            | x3 ⇒ pairT exadecim bool x9 false
-            | x4 ⇒ pairT exadecim bool xA false
-            | x5 ⇒ pairT exadecim bool xB false
-            | x6 ⇒ pairT exadecim bool xC false
-            | x7 ⇒ pairT exadecim bool xD false
-            | x8 ⇒ pairT exadecim bool xE false
-            | x9 ⇒ pairT exadecim bool xF false
-            | xA ⇒ pairT exadecim bool x0 true
-            | xB ⇒ pairT exadecim bool x1 true
-            | xC ⇒ pairT exadecim bool x2 true
-            | xD ⇒ pairT exadecim bool x3 true
-            | xE ⇒ pairT exadecim bool x4 true
-            | xF ⇒ pairT exadecim bool x5 true ] 
+            [ x0 ⇒ pair exadecim bool x6 false
+            | x1 ⇒ pair exadecim bool x7 false
+            | x2 ⇒ pair exadecim bool x8 false
+            | x3 ⇒ pair exadecim bool x9 false
+            | x4 ⇒ pair exadecim bool xA false
+            | x5 ⇒ pair exadecim bool xB false
+            | x6 ⇒ pair exadecim bool xC false
+            | x7 ⇒ pair exadecim bool xD false
+            | x8 ⇒ pair exadecim bool xE false
+            | x9 ⇒ pair exadecim bool xF false
+            | xA ⇒ pair exadecim bool x0 true
+            | xB ⇒ pair exadecim bool x1 true
+            | xC ⇒ pair exadecim bool x2 true
+            | xD ⇒ pair exadecim bool x3 true
+            | xE ⇒ pair exadecim bool x4 true
+            | xF ⇒ pair exadecim bool x5 true ] 
        | x7 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x7 false
-            | x1 ⇒ pairT exadecim bool x8 false
-            | x2 ⇒ pairT exadecim bool x9 false
-            | x3 ⇒ pairT exadecim bool xA false
-            | x4 ⇒ pairT exadecim bool xB false
-            | x5 ⇒ pairT exadecim bool xC false
-            | x6 ⇒ pairT exadecim bool xD false
-            | x7 ⇒ pairT exadecim bool xE false
-            | x8 ⇒ pairT exadecim bool xF false
-            | x9 ⇒ pairT exadecim bool x0 true
-            | xA ⇒ pairT exadecim bool x1 true
-            | xB ⇒ pairT exadecim bool x2 true
-            | xC ⇒ pairT exadecim bool x3 true
-            | xD ⇒ pairT exadecim bool x4 true
-            | xE ⇒ pairT exadecim bool x5 true
-            | xF ⇒ pairT exadecim bool x6 true ] 
+            [ x0 ⇒ pair exadecim bool x7 false
+            | x1 ⇒ pair exadecim bool x8 false
+            | x2 ⇒ pair exadecim bool x9 false
+            | x3 ⇒ pair exadecim bool xA false
+            | x4 ⇒ pair exadecim bool xB false
+            | x5 ⇒ pair exadecim bool xC false
+            | x6 ⇒ pair exadecim bool xD false
+            | x7 ⇒ pair exadecim bool xE false
+            | x8 ⇒ pair exadecim bool xF false
+            | x9 ⇒ pair exadecim bool x0 true
+            | xA ⇒ pair exadecim bool x1 true
+            | xB ⇒ pair exadecim bool x2 true
+            | xC ⇒ pair exadecim bool x3 true
+            | xD ⇒ pair exadecim bool x4 true
+            | xE ⇒ pair exadecim bool x5 true
+            | xF ⇒ pair exadecim bool x6 true ] 
        | x8 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x8 false
-            | x1 ⇒ pairT exadecim bool x9 false
-            | x2 ⇒ pairT exadecim bool xA false
-            | x3 ⇒ pairT exadecim bool xB false
-            | x4 ⇒ pairT exadecim bool xC false
-            | x5 ⇒ pairT exadecim bool xD false
-            | x6 ⇒ pairT exadecim bool xE false
-            | x7 ⇒ pairT exadecim bool xF false
-            | x8 ⇒ pairT exadecim bool x0 true
-            | x9 ⇒ pairT exadecim bool x1 true
-            | xA ⇒ pairT exadecim bool x2 true
-            | xB ⇒ pairT exadecim bool x3 true
-            | xC ⇒ pairT exadecim bool x4 true
-            | xD ⇒ pairT exadecim bool x5 true
-            | xE ⇒ pairT exadecim bool x6 true
-            | xF ⇒ pairT exadecim bool x7 true ] 
+            [ x0 ⇒ pair exadecim bool x8 false
+            | x1 ⇒ pair exadecim bool x9 false
+            | x2 ⇒ pair exadecim bool xA false
+            | x3 ⇒ pair exadecim bool xB false
+            | x4 ⇒ pair exadecim bool xC false
+            | x5 ⇒ pair exadecim bool xD false
+            | x6 ⇒ pair exadecim bool xE false
+            | x7 ⇒ pair exadecim bool xF false
+            | x8 ⇒ pair exadecim bool x0 true
+            | x9 ⇒ pair exadecim bool x1 true
+            | xA ⇒ pair exadecim bool x2 true
+            | xB ⇒ pair exadecim bool x3 true
+            | xC ⇒ pair exadecim bool x4 true
+            | xD ⇒ pair exadecim bool x5 true
+            | xE ⇒ pair exadecim bool x6 true
+            | xF ⇒ pair exadecim bool x7 true ] 
        | x9 ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool x9 false
-            | x1 ⇒ pairT exadecim bool xA false
-            | x2 ⇒ pairT exadecim bool xB false
-            | x3 ⇒ pairT exadecim bool xC false
-            | x4 ⇒ pairT exadecim bool xD false
-            | x5 ⇒ pairT exadecim bool xE false
-            | x6 ⇒ pairT exadecim bool xF false
-            | x7 ⇒ pairT exadecim bool x0 true
-            | x8 ⇒ pairT exadecim bool x1 true
-            | x9 ⇒ pairT exadecim bool x2 true
-            | xA ⇒ pairT exadecim bool x3 true
-            | xB ⇒ pairT exadecim bool x4 true
-            | xC ⇒ pairT exadecim bool x5 true
-            | xD ⇒ pairT exadecim bool x6 true
-            | xE ⇒ pairT exadecim bool x7 true
-            | xF ⇒ pairT exadecim bool x8 true ] 
+            [ x0 ⇒ pair exadecim bool x9 false
+            | x1 ⇒ pair exadecim bool xA false
+            | x2 ⇒ pair exadecim bool xB false
+            | x3 ⇒ pair exadecim bool xC false
+            | x4 ⇒ pair exadecim bool xD false
+            | x5 ⇒ pair exadecim bool xE false
+            | x6 ⇒ pair exadecim bool xF false
+            | x7 ⇒ pair exadecim bool x0 true
+            | x8 ⇒ pair exadecim bool x1 true
+            | x9 ⇒ pair exadecim bool x2 true
+            | xA ⇒ pair exadecim bool x3 true
+            | xB ⇒ pair exadecim bool x4 true
+            | xC ⇒ pair exadecim bool x5 true
+            | xD ⇒ pair exadecim bool x6 true
+            | xE ⇒ pair exadecim bool x7 true
+            | xF ⇒ pair exadecim bool x8 true ] 
        | xA ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool xA false
-            | x1 ⇒ pairT exadecim bool xB false
-            | x2 ⇒ pairT exadecim bool xC false
-            | x3 ⇒ pairT exadecim bool xD false
-            | x4 ⇒ pairT exadecim bool xE false
-            | x5 ⇒ pairT exadecim bool xF false
-            | x6 ⇒ pairT exadecim bool x0 true
-            | x7 ⇒ pairT exadecim bool x1 true
-            | x8 ⇒ pairT exadecim bool x2 true
-            | x9 ⇒ pairT exadecim bool x3 true
-            | xA ⇒ pairT exadecim bool x4 true
-            | xB ⇒ pairT exadecim bool x5 true
-            | xC ⇒ pairT exadecim bool x6 true
-            | xD ⇒ pairT exadecim bool x7 true
-            | xE ⇒ pairT exadecim bool x8 true
-            | xF ⇒ pairT exadecim bool x9 true ] 
+            [ x0 ⇒ pair exadecim bool xA false
+            | x1 ⇒ pair exadecim bool xB false
+            | x2 ⇒ pair exadecim bool xC false
+            | x3 ⇒ pair exadecim bool xD false
+            | x4 ⇒ pair exadecim bool xE false
+            | x5 ⇒ pair exadecim bool xF false
+            | x6 ⇒ pair exadecim bool x0 true
+            | x7 ⇒ pair exadecim bool x1 true
+            | x8 ⇒ pair exadecim bool x2 true
+            | x9 ⇒ pair exadecim bool x3 true
+            | xA ⇒ pair exadecim bool x4 true
+            | xB ⇒ pair exadecim bool x5 true
+            | xC ⇒ pair exadecim bool x6 true
+            | xD ⇒ pair exadecim bool x7 true
+            | xE ⇒ pair exadecim bool x8 true
+            | xF ⇒ pair exadecim bool x9 true ] 
        | xB ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool xB false
-            | x1 ⇒ pairT exadecim bool xC false
-            | x2 ⇒ pairT exadecim bool xD false
-            | x3 ⇒ pairT exadecim bool xE false
-            | x4 ⇒ pairT exadecim bool xF false
-            | x5 ⇒ pairT exadecim bool x0 true
-            | x6 ⇒ pairT exadecim bool x1 true
-            | x7 ⇒ pairT exadecim bool x2 true
-            | x8 ⇒ pairT exadecim bool x3 true
-            | x9 ⇒ pairT exadecim bool x4 true
-            | xA ⇒ pairT exadecim bool x5 true
-            | xB ⇒ pairT exadecim bool x6 true
-            | xC ⇒ pairT exadecim bool x7 true
-            | xD ⇒ pairT exadecim bool x8 true
-            | xE ⇒ pairT exadecim bool x9 true
-            | xF ⇒ pairT exadecim bool xA true ] 
+            [ x0 ⇒ pair exadecim bool xB false
+            | x1 ⇒ pair exadecim bool xC false
+            | x2 ⇒ pair exadecim bool xD false
+            | x3 ⇒ pair exadecim bool xE false
+            | x4 ⇒ pair exadecim bool xF false
+            | x5 ⇒ pair exadecim bool x0 true
+            | x6 ⇒ pair exadecim bool x1 true
+            | x7 ⇒ pair exadecim bool x2 true
+            | x8 ⇒ pair exadecim bool x3 true
+            | x9 ⇒ pair exadecim bool x4 true
+            | xA ⇒ pair exadecim bool x5 true
+            | xB ⇒ pair exadecim bool x6 true
+            | xC ⇒ pair exadecim bool x7 true
+            | xD ⇒ pair exadecim bool x8 true
+            | xE ⇒ pair exadecim bool x9 true
+            | xF ⇒ pair exadecim bool xA true ] 
        | xC ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool xC false
-            | x1 ⇒ pairT exadecim bool xD false
-            | x2 ⇒ pairT exadecim bool xE false
-            | x3 ⇒ pairT exadecim bool xF false
-            | x4 ⇒ pairT exadecim bool x0 true
-            | x5 ⇒ pairT exadecim bool x1 true
-            | x6 ⇒ pairT exadecim bool x2 true
-            | x7 ⇒ pairT exadecim bool x3 true
-            | x8 ⇒ pairT exadecim bool x4 true
-            | x9 ⇒ pairT exadecim bool x5 true
-            | xA ⇒ pairT exadecim bool x6 true
-            | xB ⇒ pairT exadecim bool x7 true
-            | xC ⇒ pairT exadecim bool x8 true
-            | xD ⇒ pairT exadecim bool x9 true
-            | xE ⇒ pairT exadecim bool xA true
-            | xF ⇒ pairT exadecim bool xB true ] 
+            [ x0 ⇒ pair exadecim bool xC false
+            | x1 ⇒ pair exadecim bool xD false
+            | x2 ⇒ pair exadecim bool xE false
+            | x3 ⇒ pair exadecim bool xF false
+            | x4 ⇒ pair exadecim bool x0 true
+            | x5 ⇒ pair exadecim bool x1 true
+            | x6 ⇒ pair exadecim bool x2 true
+            | x7 ⇒ pair exadecim bool x3 true
+            | x8 ⇒ pair exadecim bool x4 true
+            | x9 ⇒ pair exadecim bool x5 true
+            | xA ⇒ pair exadecim bool x6 true
+            | xB ⇒ pair exadecim bool x7 true
+            | xC ⇒ pair exadecim bool x8 true
+            | xD ⇒ pair exadecim bool x9 true
+            | xE ⇒ pair exadecim bool xA true
+            | xF ⇒ pair exadecim bool xB true ] 
        | xD ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool xD false
-            | x1 ⇒ pairT exadecim bool xE false
-            | x2 ⇒ pairT exadecim bool xF false
-            | x3 ⇒ pairT exadecim bool x0 true
-            | x4 ⇒ pairT exadecim bool x1 true
-            | x5 ⇒ pairT exadecim bool x2 true
-            | x6 ⇒ pairT exadecim bool x3 true
-            | x7 ⇒ pairT exadecim bool x4 true
-            | x8 ⇒ pairT exadecim bool x5 true
-            | x9 ⇒ pairT exadecim bool x6 true
-            | xA ⇒ pairT exadecim bool x7 true
-            | xB ⇒ pairT exadecim bool x8 true
-            | xC ⇒ pairT exadecim bool x9 true
-            | xD ⇒ pairT exadecim bool xA true
-            | xE ⇒ pairT exadecim bool xB true
-            | xF ⇒ pairT exadecim bool xC true ] 
+            [ x0 ⇒ pair exadecim bool xD false
+            | x1 ⇒ pair exadecim bool xE false
+            | x2 ⇒ pair exadecim bool xF false
+            | x3 ⇒ pair exadecim bool x0 true
+            | x4 ⇒ pair exadecim bool x1 true
+            | x5 ⇒ pair exadecim bool x2 true
+            | x6 ⇒ pair exadecim bool x3 true
+            | x7 ⇒ pair exadecim bool x4 true
+            | x8 ⇒ pair exadecim bool x5 true
+            | x9 ⇒ pair exadecim bool x6 true
+            | xA ⇒ pair exadecim bool x7 true
+            | xB ⇒ pair exadecim bool x8 true
+            | xC ⇒ pair exadecim bool x9 true
+            | xD ⇒ pair exadecim bool xA true
+            | xE ⇒ pair exadecim bool xB true
+            | xF ⇒ pair exadecim bool xC true ] 
        | xE ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool xE false
-            | x1 ⇒ pairT exadecim bool xF false
-            | x2 ⇒ pairT exadecim bool x0 true
-            | x3 ⇒ pairT exadecim bool x1 true
-            | x4 ⇒ pairT exadecim bool x2 true
-            | x5 ⇒ pairT exadecim bool x3 true
-            | x6 ⇒ pairT exadecim bool x4 true
-            | x7 ⇒ pairT exadecim bool x5 true
-            | x8 ⇒ pairT exadecim bool x6 true
-            | x9 ⇒ pairT exadecim bool x7 true
-            | xA ⇒ pairT exadecim bool x8 true
-            | xB ⇒ pairT exadecim bool x9 true
-            | xC ⇒ pairT exadecim bool xA true
-            | xD ⇒ pairT exadecim bool xB true
-            | xE ⇒ pairT exadecim bool xC true
-            | xF ⇒ pairT exadecim bool xD true ] 
+            [ x0 ⇒ pair exadecim bool xE false
+            | x1 ⇒ pair exadecim bool xF false
+            | x2 ⇒ pair exadecim bool x0 true
+            | x3 ⇒ pair exadecim bool x1 true
+            | x4 ⇒ pair exadecim bool x2 true
+            | x5 ⇒ pair exadecim bool x3 true
+            | x6 ⇒ pair exadecim bool x4 true
+            | x7 ⇒ pair exadecim bool x5 true
+            | x8 ⇒ pair exadecim bool x6 true
+            | x9 ⇒ pair exadecim bool x7 true
+            | xA ⇒ pair exadecim bool x8 true
+            | xB ⇒ pair exadecim bool x9 true
+            | xC ⇒ pair exadecim bool xA true
+            | xD ⇒ pair exadecim bool xB true
+            | xE ⇒ pair exadecim bool xC true
+            | xF ⇒ pair exadecim bool xD true ] 
        | xF ⇒
            match e2 with
-            [ x0 ⇒ pairT exadecim bool xF false
-            | x1 ⇒ pairT exadecim bool x0 true
-            | x2 ⇒ pairT exadecim bool x1 true
-            | x3 ⇒ pairT exadecim bool x2 true
-            | x4 ⇒ pairT exadecim bool x3 true
-            | x5 ⇒ pairT exadecim bool x4 true
-            | x6 ⇒ pairT exadecim bool x5 true
-            | x7 ⇒ pairT exadecim bool x6 true
-            | x8 ⇒ pairT exadecim bool x7 true
-            | x9 ⇒ pairT exadecim bool x8 true
-            | xA ⇒ pairT exadecim bool x9 true
-            | xB ⇒ pairT exadecim bool xA true
-            | xC ⇒ pairT exadecim bool xB true
-            | xD ⇒ pairT exadecim bool xC true
-            | xE ⇒ pairT exadecim bool xD true
-            | xF ⇒ pairT exadecim bool xE true ]
+            [ x0 ⇒ pair exadecim bool xF false
+            | x1 ⇒ pair exadecim bool x0 true
+            | x2 ⇒ pair exadecim bool x1 true
+            | x3 ⇒ pair exadecim bool x2 true
+            | x4 ⇒ pair exadecim bool x3 true
+            | x5 ⇒ pair exadecim bool x4 true
+            | x6 ⇒ pair exadecim bool x5 true
+            | x7 ⇒ pair exadecim bool x6 true
+            | x8 ⇒ pair exadecim bool x7 true
+            | x9 ⇒ pair exadecim bool x8 true
+            | xA ⇒ pair exadecim bool x9 true
+            | xB ⇒ pair exadecim bool xA true
+            | xC ⇒ pair exadecim bool xB true
+            | xD ⇒ pair exadecim bool xC true
+            | xE ⇒ pair exadecim bool xD true
+            | xF ⇒ pair exadecim bool xE true ]
        ]
    ].
 
 (* operatore somma senza carry *)
 definition plus_exnc ≝
-λe1,e2:exadecim.fstT ?? (plus_ex e1 e2 false).
+λe1,e2:exadecim.fst ?? (plus_ex e1 e2 false).
 
 (* operatore carry della somma *)
 definition plus_exc ≝
-λe1,e2:exadecim.sndT ?? (plus_ex e1 e2 false).
+λe1,e2:exadecim.snd ?? (plus_ex e1 e2 false).
 
 (* operatore Most Significant Bit *)
 definition MSB_ex ≝
@@ -1637,7 +1637,7 @@ qed.
 lemma plusex_ok:
  ∀b1,b2,c.
   match plus_ex b1 b2 c with
-   [ pairT r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecim r + nat_of_bool c' * 16 ].
+   [ pair r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecim r + nat_of_bool c' * 16 ].
  intros;
  elim b1; (elim b2; (elim c; normalize; reflexivity)).
 qed.
@@ -1745,7 +1745,7 @@ lemma ok_succ_ex : ∀e:exadecim.
 
 lemma ok_rcr_ex : ∀e:exadecim.∀b:bool.
  rcr_ex e b = 
- pairT exadecim bool
+ pair exadecim bool
   (exadecim_of_nat ((e/2)+match b with [ true ⇒ 8 | false ⇒ 0]))
   (eqb (mod e 2) 1).
  intros;
@@ -1760,7 +1760,7 @@ qed.
 
 lemma ok_rcl_ex : ∀e:exadecim.∀b:bool.
  rcl_ex e b =
- pairT exadecim bool
+ pair exadecim bool
   (exadecim_of_nat ((mod (e*2) 16)+match b with [ true ⇒ 1 | false ⇒ 0]))
   (notb (ltb e 8)).
  intros;
@@ -1776,7 +1776,7 @@ lemma ok_rcl_ex : ∀e:exadecim.∀b:bool.
 
 lemma ok_shr_ex : ∀e:exadecim.
  shr_ex e =
- pairT exadecim bool
+ pair exadecim bool
   (exadecim_of_nat (e/2))
   (eqb (mod e 2) 1).
  intros;
@@ -1789,7 +1789,7 @@ qed.
 
 lemma ok_shl_ex : ∀e:exadecim.
  shl_ex e =
- pairT exadecim bool
+ pair exadecim bool
   (exadecim_of_nat (mod (e*2) 16))
   (notb (ltb e 8)).
  intros;