proposition: Lemma accept_any_inv: forall s, s \in r_any -> exists c, s = [c].
proof: Proof. intros. unfold r_any in *. apply union_inv in H. destruct H as (r, (Hi, Hs)). apply all_chars_inv in Hi. destruct Hi as (c, Hi). subst. inversion Hs; subst. eauto. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang