proposition: Lemma allseq_dec (p : pred rT) : decidable (forall x, p (f x)).
proof: Proof. case: (exseq_dec (predC p)) => H;[right|left]. - move => A. case: H => [x /= Hx]. by rewrite A in Hx. - move => x. apply/negPn/negP => C. apply: H. by exists x. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)