proposition: Lemma Prf_CoCone_nt_law : CoCone_law -> NT_law (G:=Const J c) T.
proof: Proof. unfold NT_law in |- *; intros H a b f. unfold FMor at 2 in |- *; simpl in |- *; unfold Const_mor in |- *. apply Trans with (T a). apply (H a b). apply Idr. Qed.
imports: Limit