proposition: Lemma sat_emptyN I X : I |= Not (empty X) <-> (exists n, n \in I X).
proof: Proof. rewrite satDN; split => [[N]|] /=. - case: (I X) => [|x IX _]. + by case/(_ _)/Wrap. + by exists x; rewrite mem_head. - case => n A. exists [:: n.+1]. move/(_ _ A). by rewrite inE ltn_eqF. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)