proposition: Lemma L_set0 p q w : L^set0 q p w -> p = q /\ w = [::] \/ exists2 a, w = [::a] & p = dfa_trans q a.
proof: Proof. case/LP => <-. case: w => [|a [|b w]] H ; [by left|by right;exists a|]. move: (H 1). do 2 case/(_ _)/Wrap => //. by rewrite inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)