fact: Fixpoint bound (s : form) : nat := match s with | Incl X Y => maxn X.+1 Y.+1 | Less X Y => maxn X.+1 Y.+1 | FF => 0 | Imp s t => maxn (bound s) (bound t) | Ex s => (bound s).-1 end.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)