proposition: Lemma Ldiese_map : forall (c : C) (tau1 tau2 : Cone c F), tau1 =_NT tau2 -> Lim_diese l tau1 =_S Lim_diese l tau2.
proof: Proof. intros c tau1 tau2 p. apply (Prf_limit2 l (tau:=tau2) (g:=Lim_diese l tau1)). unfold Limit_eq in |- *; intro i. apply Trans with (tau1 i). apply (Prf_limit1 l tau1). apply (p i). Qed.
imports: Const CoUniversalArrow Ntransformation