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;
*)
+*)