(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LOGIC/NTrack/order".
+
include "Track/order.ma".
include "NTrack/props.ma".
(* Order properties *********************************************************)
-
+(*
theorem ntrack_refl: \forall P. \forall c:Formula. \exists r.
NTrack P r (pair c c).
intros; elim c; clear c;
lapply linear ntrack_track to H1 as H;
lapply linear track_trans to H0, H as H1; decompose;
*)
+*)