fact: Fixpoint e_level e := match e with | e_bot => BOT | e_top => TOP | e_cup x y => CUP + e_level x + e_level y | e_cap x y => CAP + e_level x + e_level y | e_neg x => BL + e_level x | e_var _ => MIN end%level.
imports: positives comparisons lattice lset sups