proposition: Lemma r_app_union_distr_l: forall r1 r2 r3, (r1 ;; r3) || (r2 ;; r3) <==> (r1 || r2) ;; r3.
proof: Proof. unfold REquiv. intros. repeat (first [ rewrite r_app_rw | rewrite r_union_rw ]). apply app_union_distr_l. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang