proposition: Lemma Comp_cone_tau_cone_law : Cone_law Comp_cone_tau.
proof: Proof. unfold Cone_law in |- *; intros i j g; unfold Comp_cone_tau in |- *. unfold FMor at 3 in |- *; simpl in |- *. unfold Comp_FMor in |- *. apply Trans with (FMor G (T i o FMor F g)). unfold Comp_FOb in |- *; apply FPres. apply (EqC T g). unfold Comp_FOb in |- *; apply FComp. Qed.
imports: Limit