proposition: Lemma prog_cup_x R R' S: prog R S -> prog R' S -> prog (R++R') S.
proof: Proof. intros H H' e f Hef. apply in_app_iff in Hef as [?|?]. now apply H. now apply H'. Qed.
imports: lset kat positives sums glang boolean comparisons powerfix ugregex