1 set "baseuri" "cic:/matita/LOGIC/CLE/defs".
3 (* ORDER RELATION BETWEEN POSITIONS AND CONTEXTS
6 include "datatypes/Context.ma".
8 inductive CLE: Nat \to Context \to Prop \def
9 | cle_zero: \forall Q. CLE zero Q
10 | cle_succ: \forall Q,i. CLE i Q \to
11 \forall p1,p2,R. CLE (succ i) (abst Q p1 p2 R)
14 interpretation "order relation between positions and contexts"
15 'leq x y = (cic:/matita/LOGIC/CLE/defs/CLE.ind#xpointer(1/1) x y).