-theorem track_weak: \forall R,p,P,Q,S,i.
- Track P p S \to Insert R i P Q \to
- \exists q. Track Q q S.
+include "Insert/props.ma".
+include "Track/defs.ma".
+include "NTrack/inv.ma".
+(*
+theorem ntrack_weak: \forall R,p,P,Q,S,i.
+ NTrack P p S \to Insert R i P Q \to
+ \exists q. NTrack Q q S.