proposition: Lemma epsilon_eval e: epsilon e = eval (X:=bool_ops) (f':=fun _ => bool_tt) (fun _ => false) (to_expr e).
proof: Proof. induction e; simpl; trivial; now rewrite IHe1, IHe2. Qed.
imports: syntax kleene boolean lang lset sums normalisation