proposition: Lemma sup_sup `{L: laws} `{BSL ≪ l} I (f: I -> X) A (J: A -> list I) h: sup f (sup J h) ≡ sup (fun a => sup f (J a)) h.
proof: Proof. induction h. reflexivity. simpl. now rewrite sup_app, IHh. Qed.
imports: lset lattice ordinal