proposition: Lemma step_fun x : functional (step M x).
proof: Proof. have lr: ((R == L = false)*(L == R = false))%type by done. move => [p i] [q j] [r k]. rewrite /step. case: (read1 p i) => [ -> |[[q' [|]] -> ]]; first by rewrite !inE. - rewrite !inE !xpair_eqE -/L -/R !lr !eqxx !andbT !andbF /=. move => /andP [/eqP -> /eqP A] /andP [/eqP -> /eqP B]. f_equal. apply ord_inj. apply/eqP. by rewrite -eqSS A B. - rewrite !inE !xpair_eqE -/L -/R !lr !eqxx !andbT !andbF !orbF /=. move => /andP [/eqP -> /eqP A] /andP [/eqP -> /eqP B]. f_equal. apply ord_inj. apply/eqP. by rewrite -eqSS A B. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa regexp myhill_nerode)