proposition: Lemma sat_all1 I s : I |= All1 s <-> (forall n, cons [:: n] I |= s).
proof: Proof. rewrite sat_all; split. - move => H n. move: (H [:: n]) => {H} /=. apply. rewrite sat_singles. by exists n. - move => H N. rewrite sat_imp sat_singles => [[n Hn]]. apply: weak_coincidence (H n). by case. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)