fact: Record strictSet := mkStrictSet { sSet_carrier :> Type ; is_strict : forall (x y : sSet_carrier), x = y -> x = y }.
imports: Coq(ssreflect ssrfun ssrbool) Coq(FunctionalExtensionality) Coq(Relation_Definitions Morphisms RelationPairs) Mon(SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory Rel)