proposition: Lemma L_monotone (X : {set A}) (x y z : A): {subset L^X x y <= L^(z |: X) x y}.
proof: Proof. move => w. rewrite !unfold_in. case: (_ == _) => //. apply: sub_forall => i /=. case: (_ < _) => //= H. by rewrite inE H orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)