the published devels must be removed from the tests

[helm.git] / helm / software / matita / contribs / LOGIC / Track / defs.ma

diff --git a/helm/software/matita/contribs/LOGIC/Track/defs.ma b/helm/software/matita/contribs/LOGIC/Track/defs.ma
index a9c4479ac328a4743d3699e8cb9077340c444a22..c5e6e69be7b9b73872c90f0b975eac7cff475b37 100644 (file)
--- a/helm/software/matita/contribs/LOGIC/Track/defs.ma
+++ b/helm/software/matita/contribs/LOGIC/Track/defs.ma
@@ -35,4 +35,8 @@ inductive Track: Context \to Proof \to Sequent \to Prop \def
                 Track Q r (pair lleaf D) \to
                 Insert (pair A B) i P Q \to
                 Track P (impi p q r) (pair (impl a b) D)
+   | track_scut: \forall P,p,q,A,B. \forall c:Formula.
+                 Track P p (pair A c) \to
+                 Track P q (pair c B) \to
+                 Track P (scut p q) (pair A B)
 .