fact: Record Bool_eq_type : Type := mkBool_eq_type { bet_type :> Type; bet_eq : bet_type -> bet_type -> bool; bet_ok : forall x y, bet_eq x y = true <-> x = y }.
imports: Coq(Structures.Equalities) CoLoR(LogicUtil RelUtil BoolUtil)