proposition: Lemma epsilon_pure e: is_pure e -> epsilon e = false.
proof: Proof. induction 1; trivial. simpl. now rewrite IHis_pure1. simpl. rewrite IHis_pure. now case epsilon. Qed.
imports: syntax kleene boolean lang lset sums normalisation