proposition: Lemma local_limit_dep_name : forall I A {IA:Inhab A} (i:I) (v:I->A) (M:family I A), locally_complete M -> locally_coherent M i v -> exists l, local_limit_dep M i (fun j _ => v j) = l /\ (forall j, family_r M j i -> family_sim M j (v j) l).
proof: Proof. Proof using. introv Loca Cohi. esplit. split. reflexivity. unfold local_limit_dep. epsilon l. forwards~ [l L]: (Loca v i). exists l. intros k. destruct_if~. intros L. intros j Rji. specializes L j. rewrite~ (classicT_l Rji) in L. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)