| xF ⇒ b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? (b8_S ? recb))))))))))))))
].
-ndefinition b8_to_recb8 ≝
-λn.b8_to_recb8_aux3 (b8h n) (b8l n) (b8_to_recb8_aux2 (b8h n) (ex_to_recex (b8h n))).
+ndefinition b8_to_recb8 : Πb.rec_byte8 b.
+ #b;
+ nletin K ≝ (b8_to_recb8_aux3 (b8h b) (b8l b) (b8_to_recb8_aux2 (b8h b) (ex_to_recex (b8h b))));
+ nelim b in K:(%) ⊢ %;
+ #e1; #e2; nnormalize; #H; napply H.
+nqed.
(* ottali → esadecimali *)
ndefinition b8_of_bit ≝