X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLOGIC%2FPRed%2Fdefs.ma;h=85a4c3bf9af0512e4ef7599cf0cdaeda1b00ac9b;hb=09c8bb55c25143efdfbd34a20bb2fe6b681760b6;hp=ef0f86194edd23dd90aa5dcf939cb133138f16d8;hpb=add325fb02ab0e46a2c7bbffb2e9c980128f0f69;p=helm.git

diff --git a/helm/software/matita/contribs/LOGIC/PRed/defs.ma b/helm/software/matita/contribs/LOGIC/PRed/defs.ma
index ef0f86194..85a4c3bf9 100644
--- a/helm/software/matita/contribs/LOGIC/PRed/defs.ma
+++ b/helm/software/matita/contribs/LOGIC/PRed/defs.ma
@@ -47,6 +47,8 @@ inductive PRed: Context \to Proof \to Sequent \to
                 \forall h. PRed P1 (scut (prin h) q1) S P2 q2 S
    | pred_b_dx: \forall p1,p2,Q1,Q2,S. PRed Q1 p1 S Q2 p2 S \to
                 \forall h. PRed Q1 (scut p1 (prin h)) S Q2 p2 S
+   | pred_c   : \forall p1,p2,Q1,Q2,S. PRed Q1 p1 S Q2 p2 S \to 
+                \forall p. PRed Q1 (scut (impr p) (impw p1)) S Q2 p2 S    
 .
 
 (*CSC: the URI must disappear: there is a bug now *)
@@ -55,3 +57,7 @@ interpretation
    'parred3 x1 y1 z1 x2 y2 z2 = 
       (cic:/matita/LOGIC/PRed/defs/PRed.ind#xpointer(1/1) x1 y1 z1 x2 y2 z2)
 .
+
+notation "hvbox([a1,b1,c1] break => [a2,b2,c2])" 
+  non associative with precedence 45
+for @{ 'parred3 $a1 $b1 $c1 $a2 $b2 $c2 }.