fact: Record family (I A : Type) : Type := { family_r : binary I; family_sim : I -> binary A }.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)