fact: Fixpoint eval e: X := match e with | e_bot => bot | e_top => top | e_cup x y => eval x ⊔ eval y | e_cap x y => eval x ⊓ eval y | e_neg x => ! eval x | e_var a => f a end.
imports: positives comparisons lattice lset sups