proposition: Lemma vec_of_valP I s : satisfies I s <-> satisfies (I_of (vec_of_val I (bound s))) s.
proof: Proof. apply: coincidence. exact: vec_of_val_agrees. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)