proposition: Lemma r_char_rw: forall c, Equiv (Accept (r_char c)) (Lang.Char c).
proof: Proof. split; intros. - inversion H; subst; clear H. apply char_in. - apply char_in_inv in H. subst. apply accept_char. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang