proposition: Lemma term_srel k x q (H: k < (size x).+2) : terminal (srel M k x) (q,inord k).
proof: Proof. move => c /=. by rewrite /srel inordK // ?eqxx /= andbF. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)