proposition: Lemma leq_ind leq weq (L: laws BKA (re_ind leq weq)) (e f: regex'): e ≦ f -> leq e f.
proof: Proof. intro H. rewrite <-(re_ind_eval leq weq e), <-(re_ind_eval leq weq f). apply (H _ L). Qed.
imports: syntax kleene boolean lang lset sums normalisation