proposition: Lemma r_star_union_nil_rw: forall r, r_star (r_nil || r) <==> r_star r.
proof: Proof. unfold REquiv. intros. repeat first [ rewrite r_star_rw | rewrite r_union_rw | rewrite r_nil_rw ]. apply star_union_nil_rw. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang