proposition: Lemma LP {X : {set A}} {p q : A} {x} : reflect (delta p x = q /\ forall i, (0 < i) -> (i < size x) -> delta p (take i x) \in X) (x \in L^X p q).
proof: Proof. apply: (iffP andP); case => /eqP ? H; split => //. - move => i I1 I2. exact: (forall_inP H (Ordinal I2)). - apply/forall_inP => [[i I1 /= I2]]; auto. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)