proposition: Lemma rex_pump_union_r: forall re1 re2 s2, RexPump re2 s2 -> RexPump (re1 || re2) s2.
proof: Proof. intros. inversion H; subst; clear H. apply rex_pump_def with (x:=x) (y:=y) (z:=z). - reflexivity. - assumption. - simpl. apply le_plus_trans_rev. assumption. - intros. apply accept_union_r. auto. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang