proposition: Lemma epsilon_iff_lang_nil a e: epsilon (set.mem a) e <-> (lang e) (tnil a).
proof: Proof. induction e; simpl. intuition discriminate. apply eq_bool_iff. simpl epsilon. induction p; simpl. reflexivity. reflexivity. rewrite <-Bool.orb_lazy_alt. congruence. rewrite <-Bool.andb_lazy_alt. congruence. congruence. reflexivity. setoid_rewrite Bool.orb_true_iff. now apply cup_weq. setoid_rewrite Bool.andb_true_iff. setoid_rewrite traces_dot_nil. now apply cap_weq. split. exists O. simpl. tauto. intros [i Hi]. rewrite IHe. clear IHe. induction i. assumption. apply IHi. setoid_rewrite traces_dot_nil in Hi. apply Hi. Qed.
imports: kat lsyntax positives sups glang comparisons boolean