+notation "14" non associative with precedence 80 for @{ 'x14 }.
+interpretation "natural number" 'x14 =
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))).
+
+notation "22" non associative with precedence 80 for @{ 'x22 }.
+interpretation "natural number" 'x22 =
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))))))))))))))))))))))).
+
+notation "256" non associative with precedence 80 for @{ 'x256 }.
+interpretation "natural number" 'x256 =
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
+(cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
+
+(*
+lemma sign_ok: ∀ n:nat. nat_of_byte (byte_of_nat n) = n \mod 256.
+ intros; elim n; [ reflexivity | unfold byte_of_nat.