proposition: Lemma sat_ex1 I s : I |= Ex1 s <-> (exists n, cons [:: n] I |= s).
proof: Proof. rewrite /Ex1; split. - case => N. rewrite -/satisfies => /sat_and [/sat_singles [n] /= B C]. exists n. apply: weak_coincidence C. by case. - case => n A. exists [:: n]. apply/sat_and;split => //. apply/sat_singles. by exists n. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)