proposition: Lemma sat_singles I X : I |= single X <-> exists n, I X =i [:: n].
proof: Proof. rewrite sat_and sat_emptyN. split. - move => [[n A] B]. exists n. move => m. rewrite inE. apply/idP/eqP => [H|-> //]. move/sat_all/(_ [:: n]): B. rewrite 2!sat_imp. case/(_ _ _)/Wrap. + rewrite sat_emptyN. exists n. by rewrite inE. + move => k /=. by rewrite inE => /eqP->. + move/(_ _ H). by rewrite inE => /eqP->. - case => n A. split; first by exists n;rewrite A mem_head. apply/sat_all => N. rewrite 2!sat_imp sat_emptyN => /= [[k Hk] D] m E. move: (D _ Hk). rewrite A inE => /eqP ?; subst. rewrite A inE in E. by rewrite (eqP E). Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)