proposition: Lemma sat_empty I X : I |= empty X <-> I X =i pred0.
proof: Proof. rewrite sat_all; split => [/= /(_ [::]) A k|A N k]; last by rewrite A. rewrite inE. apply: negbTE. apply/negP. by move/A. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)