proposition: Lemma sub_run x C (i : pos x) : reject_cert C -> {subset run_table x i <= C i}.
proof: Proof. case => T1 T2 T3 p. rewrite inE. case/connectP => cs. elim/last_ind: cs p i => /= [p i _|cs c IH p i]; first by case => -> ->. rewrite rcons_path last_rcons [last _ _]surjective_pairing => /andP [pth stp] E. subst. apply: T3 stp. by apply: IH; rewrite -?surjective_pairing. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages nfa two_way)