proposition: Lemma is_true_sup I J (f: I -> bool): \sup_(i\in J) f i <-> (exists i, List.In i J /\ f i).
proof: Proof. unfold is_true. induction J; simpl. firstorder; discriminate. rewrite Bool.orb_true_iff. firstorder congruence. Qed.
imports: monoid prop sups