proposition: Lemma Eq_cone : forall tau : Cone, Cone_law (ApNT tau).
proof: Proof. unfold Cone_law in |- *; intros tau i j g. apply Trans with (Id c o tau j). apply Idl1. apply (Prf_NT_law tau g). Qed.
imports: Const CoUniversalArrow Ntransformation