Require Import Relations. Section impredicative_eq. Variable A : Set. Set Implicit Arguments. Definition impredicative_eq (a b:A) : Prop := forall P:A -> Prop, P a -> P b. Theorem impredicative_eq_sym : symmetric A impredicative_eq. Proof. unfold symmetric, impredicative_eq; intros a b H Q. apply H; trivial. Qed. Theorem impredicative_eq_refl : reflexive A impredicative_eq. Proof. unfold reflexive, impredicative_eq; auto. Qed. Theorem impredicative_eq_trans : transitive A impredicative_eq. Proof. unfold transitive. intros x y z Hxy Hyz; unfold impredicative_eq; intros. apply Hyz. apply Hxy; assumption. Qed. Hint Resolve impredicative_eq_trans impredicative_eq_sym impredicative_eq_refl: sets. Theorem impredicative_eq_equiv : equiv A impredicative_eq. Proof. unfold equiv; auto with sets. Qed. Theorem impredicative_eq_least : forall R:relation A, reflexive A R -> inclusion A impredicative_eq R. Proof. unfold inclusion, impredicative_eq; intros R H x y H0. apply H0. apply H. Qed. Theorem impredicative_eq_eq : forall a b:A, impredicative_eq a b -> a = b. Proof. intros. apply H. trivial. Qed. Theorem eq_impredicative_eq : forall a b:A, a = b -> impredicative_eq a b. Proof. intros a b e; rewrite e; unfold impredicative_eq; auto. Qed. Theorem impredicative_eq_ind : forall (x:A) (P:A -> Prop), P x -> forall y:A, impredicative_eq x y -> P y. Proof. intros. apply H0. assumption. Qed. Set Strict Implicit. Unset Implicit Arguments. End impredicative_eq.