Library set

Require Import ext.

Definition set {A} := A → Prop.

Definition Inter {A} (R S : @set A) : set := fun a ⇒ R a ∧ S a.
Hint Unfold Inter.

Definition Cmp {A} (R : @set A) : set := fun a ⇒ ¬ R a.
Hint Unfold Cmp.

Definition Union {A} (R S : @set A) : set := fun a ⇒ R a ∨ S a.
Hint Unfold Union.

Definition Inc {A} (R S : @set A) := ∀ a, R a → S a.
Hint Unfold Inc.

Definition Eq {A} (R S : @set A) := Inc R S ∧ Inc S R.
Hint Unfold Eq.

Lemma extEq : ∀ {A} (R S : @set A), Eq R S → R = S.
Proof. intros A R S [RS SR].
apply functional_extensionality; intros x.
apply propositional_extensionality; split; auto.
Qed.