1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/defs".
18 - Usage: invoke with positive polarity
21 include "Term/defs.ma".
23 inductive Lift (l: Nat): Nat \to Term \to Term \to Prop \def
24 | lift_sort : \forall i,h.
25 Lift l i (leaf (sort h)) (leaf (sort h))
26 | lift_lref_gt: \forall i,j. i > j \to
27 Lift l i (leaf (lref j)) (leaf (lref j))
28 | lift_lref_le: \forall i,j1. i <= j1 \to
29 \forall j2. (l + j1 == j2) \to
30 Lift l i (leaf (lref j1)) (leaf (lref j2))
31 | lift_bind : \forall i,u1,u2. Lift l i u1 u2 \to
32 \forall t1,t2. Lift l (succ i) t1 t2 \to
33 \forall r. Lift l i (intb r u1 t1) (intb r u2 t2)
34 | lift_flat : \forall i,u1,u2. Lift l i u1 u2 \to
35 \forall t1,t2. Lift l i t1 t2 \to
36 \forall r. Lift l i (intf r u1 t1) (intf r u2 t2)