fact: Record OFE I A (M:family I A) := { ofe_wf : wf (family_r M); ofe_trans : trans (family_r M); ofe_equiv : forall i, equiv (family_sim M i) }.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)