proposition: Lemma make_COFE : forall I A {IA:Inhab A} (M:family I A), wf (family_r M) -> trans (family_r M) -> (forall i, equiv (family_sim M i)) -> complete M -> COFE M.
proof: Proof. Proof using. intros. asserts: (OFE M). constructor~. constructor~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)