proposition: Lemma complete_to_globally_complete : forall I A (M:family I A), OFE M -> complete M -> globally_complete M.
proof: Proof. Proof using. introv Ofem Comp Cohu. apply~ Comp. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)