proposition: Lemma Tc_limconeF_cone_law : Cone_law Tc_limconeF_tau.
proof: Proof. unfold Cone_law in |- *; simpl in |- *. intros i j g. unfold Equal_com_arrow in |- *; simpl in |- *. unfold Comp_com_mor in |- *; simpl in |- *. apply (Eq_cone (Limiting_cone l_F') g). Qed.
imports: Pres_Limits Comma_proj