started the Proof Weight predicate for cut elimination and confluence

[helm.git] / matita / contribs / LOGIC / Track / pred.ma

diff --git a/matita/contribs/LOGIC/Track/pred.ma b/matita/contribs/LOGIC/Track/pred.ma
index 3b640b97c47682a376a5990f71ce307fdea6cfac..c7f6198f95f01e9fedcefdce6c33504223a60892 100644 (file)
--- a/matita/contribs/LOGIC/Track/pred.ma
+++ b/matita/contribs/LOGIC/Track/pred.ma
@@ -36,5 +36,8 @@ theorem track_pred: \forall Q1,Q2,p1,p2,S1,S2. PRed Q1 p1 S1 Q2 p2 S2 \to
    lapply linear track_inv_prin to H5; subst; autobatch
  | lapply linear track_inv_scut to H3; decompose; subst;
    lapply linear track_inv_prin to H4; subst; autobatch
+ | lapply linear track_inv_scut to H3; decompose; subst;
+   lapply linear track_inv_impw to H4; decompose; subst;
+   lapply linear track_inv_impr to H5; decompose; subst; autobatch
  ].
 qed.