proposition: Lemma Tab_refines : refines (nfa2_lang M) Tab.
proof: Proof. move => x y E. wlog suff W: x y E / (x \in nfa2_lang M) -> (y \in nfa2_lang M). { by apply/idP/idP; exact: W. } case/exists_inP => f Hq1 Hq2. apply/exists_inP; exists f => //. move: Hq2. rewrite -[x]cats0 -[y]cats0 -!(eq_connect (@srel_step_max _)). case/(@srel_mid (size x).+1); ssrlia => q /Tab1P q1 q2. apply/(@srel_mid (size y).+1); ssrlia. - exists q. apply/Tab1P. by rewrite -E. - move: q2 => {q1}. rewrite !inord_max. apply: (runR_eq (i := 1) (j := 1) (k := 1)); rewrite ?addn1 ?cats0 //=. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)