X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FLOGIC%2FCLE%2Fdefs.ma;fp=matita%2Fcontribs%2FLOGIC%2FCLE%2Fdefs.ma;h=31bd7694e02e58e59e25088a1e68d7ea9bad03a1;hb=4d3fcebb0b24901b69f54d0eaf067885a80dcae0;hp=7a2c7606caf79d7b86c82b110d4e30159cf05755;hpb=2a85b279378df4193bbe927e3cdbaffd7d229279;p=helm.git

diff --git a/matita/contribs/LOGIC/CLE/defs.ma b/matita/contribs/LOGIC/CLE/defs.ma
index 7a2c7606c..31bd7694e 100644
--- a/matita/contribs/LOGIC/CLE/defs.ma
+++ b/matita/contribs/LOGIC/CLE/defs.ma
@@ -7,7 +7,8 @@ include "datatypes/Context.ma".
 
 inductive CLE: Nat \to Context \to Prop \def
    | cle_zero: \forall Q. CLE zero Q
-   | cle_succ: \forall Q,R,i. CLE i Q \to CLE (succ i) (abst Q R)
+   | cle_succ: \forall Q,i. CLE i Q \to 
+               \forall p1,p2,R. CLE (succ i) (abst Q p1 p2 R)
 .
 
 interpretation "order relation between positions and contexts"