proposition: Lemma is_true_inf I J (f: I -> bool): \inf_(i\in J) f i <-> (forall i, List.In i J -> f i).
proof: Proof. unfold is_true. induction J; simpl. firstorder. rewrite Bool.andb_true_iff. firstorder congruence. Qed.
imports: monoid prop sups