proposition: Lemma sat_all I s : I |= All s <-> (forall N, satisfies (cons N I) s).
proof: Proof. split => [A N|A]. - apply: satNNPP => B. apply: A. by exists N. - case: (satisfies_dec I (Ex (Not s))) => //= [[N B]]. exfalso. exact: B. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)