proposition: Lemma ugregex_compare_spec x y: compare_spec (x=y) (ugregex_compare x y).
proof: Proof. revert y; induction x; destruct y; try (constructor; congruence); simpl. case cmp_spec; constructor; congruence. case cmp_spec; constructor; congruence. eapply lex_spec; eauto. intuition congruence. eapply lex_spec; eauto. intuition congruence. case IHx; constructor; congruence. Qed.
imports: kat lsyntax positives sups glang comparisons boolean