proposition: Lemma in_sup A I J (f: I -> list A) a: In a (sup f J) <-> exists i, In i J /\ In a (f i).
proof: Proof. induction J; simpl. firstorder. rewrite in_app_iff, IHJ. clear. firstorder congruence. Qed.
imports: lset lattice ordinal