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