proposition: Lemma f_sup_weq {X: ops} {Y l} {L: laws l Y} `{Hl: CUP ≪ l} (f: X -> Y): (f bot ≡ bot) -> (forall x y, f (x ⊔ y) ≡ f x ⊔ f y) -> forall I J (g: I -> X), f (sup g J) ≡ \sup_(i\in J) f (g i).
proof: Proof. intros Hbot Hcup I J g. induction J. apply Hbot. simpl. rewrite Hcup. now apply cup_weq. Qed.
imports: lset lattice ordinal