proposition: Lemma all_chars_inv: forall r, In r all_chars -> exists c, r = r_char c.
proof: Proof. unfold all_chars; intros. rewrite in_map_iff in *. destruct H as (x, (Hc, Hi)). subst. exists x. reflexivity. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang