proposition: Lemma sat_and I s t : I |= And s t <-> (I |= s /\ I |= t).
proof: Proof. rewrite /And /Not /=. split => [A|]; last tauto. split; apply: satNNPP; tauto. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)