proposition: Lemma in_all_ascii: forall (a:ascii), List.In a all_ascii.
proof: Proof. intros. unfold all_ascii. rewrite in_map_iff. exists (nat_of_ascii a). rewrite ascii_nat_embedding. split; auto. apply in_count. auto using nat_ascii_bounded. Qed.
imports: Coq.Arith.Plus Coq.Arith.PeanoNat Coq.Lists.List