proposition: Lemma functional_srel k w : functional (srel M k w).
proof: Proof. apply: functional_sub (@srel_step _ _ k w). exact: step_fun. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)