proposition: Lemma similar_equiv : forall I A (M:family I A), OFE M -> equiv (similar M).
proof: Proof. Proof using. introv Ofe. lets: (ofe_equiv Ofe). constructor; intros_all. apply~ refl_inv. apply~ sym_inv. apply~ trans_inv. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)