[ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3
| o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ].
-coercion cic:/matita/freescale/aux_bases/exadecim_of_oct.con.
+coercion exadecim_of_oct.
(* iteratore sugli ottali *)
definition forall_oct ≝ λP.
| t18 ⇒ 〈x1,x8〉 | t19 ⇒ 〈x1,x9〉 | t1A ⇒ 〈x1,xA〉 | t1B ⇒ 〈x1,xB〉
| t1C ⇒ 〈x1,xC〉 | t1D ⇒ 〈x1,xD〉 | t1E ⇒ 〈x1,xE〉 | t1F ⇒ 〈x1,xF〉 ].
-coercion cic:/matita/freescale/aux_bases/byte8_of_bitrigesim.con.
+coercion byte8_of_bitrigesim.
(* iteratore sui bitrigesimali *)
definition forall_bitrigesim ≝ λP.