proposition: Lemma runR_eq x y z p q (i j: nat) k xk xi xj yk yi yj : Tab x = Tab y -> i <= (size z).+1 -> 0 < j <= (size z).+1 -> xk = (size x).+1 + k -> xi = size x + i -> xj = size x + j -> yk = (size y).+1 + k -> yi = size y + i -> yj = size y + j -> connect (srel xk (x++z)) (p,inord xi) (q,inord xj) -> connect (srel yk (y++z)) (p,inord yi) (q,inord yj).
proof: Proof. move => ? ? ? ? ? ? ? ? ?. subst. exact: runR. Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)