proposition: Lemma Tab1_uniq x p q : p \in (Tab M x).1 -> q \in (Tab M x).1 -> p = q.
proof: Proof. rewrite !inE => H1 H2. suff: (p,@ord_max (size x).+1) = (q,ord_max) by case. apply: term_uniq H1 H2; rewrite ?inord_max; auto using term_srel, functional_srel. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)