(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LOGIC/Track/order".
+
include "Insert/fun.ma".
include "Track/defs.ma".
(* Order properties *********************************************************)
-
+(*
theorem track_refl: \forall P. \forall c:Formula. \exists r.
Track P r (pair c c).
intros; elim c; clear c;
\exists r. Track P r (pair A B).
intros; autobatch.
qed.
+*)