bug fix in Track definition

[helm.git] / matita / contribs / LOGIC / NTrack / inv.ma

diff --git a/matita/contribs/LOGIC/NTrack/inv.ma b/matita/contribs/LOGIC/NTrack/inv.ma
index 9f334f19f81c5dd3682e3e73e54fa0e0a2bf56a3..6c57c2040417633032f1581694cb2b58d1dbf668 100644 (file)
--- a/matita/contribs/LOGIC/NTrack/inv.ma
+++ b/matita/contribs/LOGIC/NTrack/inv.ma
@@ -15,7 +15,7 @@
 set "baseuri" "cic:/matita/LOGIC/NTrack/inv".
 
 include "NTrack/defs.ma".
-
+(*
 theorem ntrack_inv_lref: \forall Q,S,i. NTrack Q (lref i) S \to
                          \exists P. Insert S i P Q.
  intros; inversion H; clear H; intros; subst; autobatch.
@@ -63,3 +63,4 @@ theorem ntrack_inv_lleaf_impl:
  | subst; autobatch depth = 4
  ].
 qed.
+*)