proposition: Lemma Prf_Cone_nt_law : Cone_law -> NT_law (F:=Const J c) T.
proof: Proof. unfold NT_law in |- *; intros H a b f. unfold FMor at 1 in |- *; simpl in |- *; unfold Const_mor in |- *. apply Trans with (T b). apply Idl. apply (H a b). Qed.
imports: Const CoUniversalArrow Ntransformation