proposition: Lemma r_union_assoc_rw: forall r1 r2 r3, r1 || (r2 || r3) <==> (r1 || r2) || r3.
proof: Proof. intros. unfold REquiv. repeat rewrite r_union_rw. apply union_assoc_rw. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang