proposition: Lemma epsilon_iff_reflexive_eps (e: regex'): epsilon e <-> 1 ≦ eps e.
proof: Proof. case epsilon. intuition. intuition. discriminate. apply lang_leq in H. specialize (H [] eq_refl). discriminate. Qed.
imports: syntax kleene boolean lang lset sums normalisation