proposition: Lemma local_limit_dep_inv : forall I A {IA:Inhab A} (i j:I) (v:I->A) (M:family I A), locally_complete M -> locally_coherent M i v -> family_r M j i -> family_sim M j (v j) (local_limit_dep M i (fun j _ => v j)).
proof: Proof. Proof using. intros. forwards~ (l&Eq&L): local_limit_dep_name. rewrite~ Eq. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)