proposition: Lemma r_union_rw: forall r1 r2, Equiv (Accept (r1 || r2)) (Lang.Union (Accept r1) (Accept r2)).
proof: Proof. unfold Equiv; split; intros. - inversion H; subst; clear H; auto using union_in_l, union_in_r. - apply union_in_inv in H. destruct H; rewrite <- Lang.in_def in *; auto using accept_union_l, accept_union_r. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang