proposition: Lemma complete_of_locally_and_globally_complete : forall I A {IA:Inhab A} (M:family I A), OFE M -> locally_complete M -> globally_complete M -> complete M.
proof: Proof. Proof using. introv IA Ofem Loca Glob Down Cohu. sets V: (fun i v' => if classicT (K i) then u i else local_limit_dep M i v'). sets v: (fix_dep V (ofe_wf Ofem)). exists (epsilon (global_limit M v)). asserts Fixv: (forall i, v i = V i (fun j _ => v j)). apply fix_dep_eq. intros x v1 v2 H. unfold V. destruct_if~. apply epsilon_eq. intros i. iff N; intros j; specializes N j; destruct (classicT (family_r M j x)); congruence. asserts LocCohv: (forall i, locally_coherent M i v). intros i. induction_wf IH: (ofe_wf Ofem) i. intros j' j Rij' Rij Rjj'. unfolds inverse. destruct (classicT (K j')) as [Kj'|NKj']. forwards~ Kj: (>> Down j' j). do 2 rewrite Fixv. unfold V. do 2 destruct_if~. rewrite (Fixv j'). unfold V. destruct_if~. apply~ local_limit_dep_inv. asserts GloCohv: (globally_coherent M v). intros i j _ _ Rji. rewrite (Fixv i). unfold V. destruct_if. forwards~ Kj: (>> Down i j). rewrite Fixv. unfold V. destruct_if~. apply~ local_limit_dep_inv. epsilon l. apply~ Glob. intros L. introv Ki. applys~ equiv_trans. rewrite Fixv. unfold V. destruct_if~. apply~ equiv_refl. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)