fact: Definition ON_cst_ok {alpha: Ord} `{OA : @ON A ltA compareA} `{OB : @ON B ltB compareB} {iota : A -> Ord} {_ : ON_correct alpha OA iota} (a: A) (b: Ord) := iota a = b.
imports: Coq(RelationClasses Relation_Operators Ensembles) hydras(OrdNotations Schutte_basics)