proposition: Lemma StringE (char : finType) (w : word char) : String w =i pred1 w.
proof: Proof. elim: w => [|a v IHv] w //=. rewrite inE /String /=. apply/concP/eqP. - move => [w1] [w2] [e []]. set r := foldr _ _ _. rewrite -/(re_lang r) inE e => /eqP -> H /=. rewrite IHv inE in H. by rewrite (eqP H). - move => e. exists [:: a]; exists v; split => //; split. by rewrite inE. by rewrite IHv inE eqxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)