fact: Definition I_of n (v : seq (n.-tuple bool)) : valuation := fun X => [seq i <- iota 0 (size v) | nth false (nth [tuple of nseq n false] v i) X].
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)