proposition: Lemma union_r_void_rw: forall (L:language), L U {} == L.
proof: Proof. split; intros. + apply union_in_inv in H. destruct H; auto. apply void_not_in in H. contradiction. + left. assumption. Qed.
imports: Coq.Lists.List