bug fix in Track definition

[helm.git] / matita / contribs / LOGIC / CLE / defs.ma

diff --git a/matita/contribs/LOGIC/CLE/defs.ma b/matita/contribs/LOGIC/CLE/defs.ma
index 7a2c7606caf79d7b86c82b110d4e30159cf05755..31bd7694e02e58e59e25088a1e68d7ea9bad03a1 100644 (file)
--- 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"