proposition: Lemma r_any_rw: Equiv (Accept r_any) Any.
proof: Proof. split; intros. - apply accept_any_inv in H. destruct H as (c, ?). subst. apply any_in. - apply any_in_inv in H. destruct H as (c, ?). rewrite <- Lang.in_def. subst. auto using accept_any. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang