proposition: Lemma cl_inf_same_set : forall (f f' : A -> Prop), (forall a, f a <-> f' a) -> eq (cl_inf f) (cl_inf f').
proof: Proof. intros. apply PO.le_antisym; eapply cl_inf_superset; intuition; eapply H; eauto. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat