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