Library Coq.ssr.ssrclasses

Compatibility layer for under and setoid_rewrite.

Note: this file does not require ssreflect; it is both required by ssrsetoid and required by ssrunder.

Redefine Coq.Classes.RelationClasses.Reflexive here, so that doing Require Import ssreflect does not Require Import RelationClasses, and conversely.

Section Defs.
  Context {A : Type}.
  Class Reflexive (R : A -> A -> Prop) :=
    reflexivity : forall x : A, R x x.
End Defs.

Instance eq_Reflexive {A : Type} : Reflexive (@eq A) := @eq_refl A.
Instance iff_Reflexive : Reflexive iff := iff_refl.

Navigation