proposition: Lemma eval_sup I (J: list I) (f: I -> expr) (X: lattice.ops) (g: A -> X): eval g (sup (X:=expr_ops) f J) = \sup_(i\in J) eval g (f i).
proof: Proof. apply f_sup_eq; now f_equal. Qed.
imports: positives comparisons lattice lset sups