proposition: Lemma ascii_beq_correct {x y} : ascii_beq x y = ascii_eq_dec x y.
proof: Proof. t ltac:(rewrite !bool_beq_correct). Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Coq.Arith.PeanoNat Coq.Strings.Ascii Coq.Strings.String Coq.Logic.Eqdep_dec Fiat.Common