proposition: Lemma ofe_sim_refl : forall I A (M:family I A) i, OFE M -> refl (family_sim M i).
proof: Proof. Proof using. intros. apply~ equiv_refl. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)