proposition: Lemma compare_letter_spec a b: compare_spec (a=b) (compare_letter a b).
proof: Proof. unfold compare_letter. case cmp_spec; intro E; constructor. now rewrite <-(plp a), <-(plp b), E. congruence. congruence. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms