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

diff --git a/matita/contribs/LOGIC/PRed/defs.ma b/matita/contribs/LOGIC/PRed/defs.ma
index ef0f86194..85a4c3bf9 100644
--- a/matita/contribs/LOGIC/PRed/defs.ma
+++ b/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 }.