matita/contribs/LOGIC/CLE/defs.ma

   1 set "baseuri" "cic:/matita/LOGIC/CLE/defs".
   2
   3 (* ORDER RELATION BETWEEN POSITIONS AND CONTEXTS
   4 *)
   5
   6 include "datatypes/Context.ma".
   7
   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)
  12 .
  13
  14 interpretation "order relation between positions and contexts"
  15    'leq x y = (cic:/matita/LOGIC/CLE/defs/CLE.ind#xpointer(1/1) x y).