proposition: Lemma L_catR X x y z w1 w2 : w1 \in L^(z |: X) x z -> w2 \in L^X z y -> w1++w2 \in L^(z |: X) x y.
proof: Proof. move => H /(L_monotone z). apply: L_cat H. exact: setU11. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)