fact: Definition L (X : {set A}) (p q : A) x := (delta p x == q) && [forall (i : 'I_(size x) | 0 < i), delta p (take i x) \in X].
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)