proposition: Lemma complete_eq_complete' : forall I A {IA:Inhab A} (M:family I A), OFE M -> (complete M = complete' M).
proof: Proof. Proof using. intros. extens. split. split. apply~ complete_to_locally_complete. apply~ complete_to_globally_complete. intros [H1 H2]. apply~ complete_of_locally_and_globally_complete. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)