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 (**************************************************************************)
16 - Usage: invoke with positive polarity
19 include "Unified-Sub/datatypes/Term.ma".
21 inductive Lift (l: Nat): Nat \to Term \to Term \to Prop \def
22 | lift_sort : \forall i,h.
23 Lift l i (sort h) (sort h)
24 | lift_lref_gt: \forall i,j. i > j \to
25 Lift l i (lref j) (lref j)
26 | lift_lref_le: \forall i,j1. i <= j1 \to
27 \forall j2. (l + j1 == j2) \to
28 Lift l i (lref j1) (lref j2)
29 | lift_bind : \forall i,u1,u2. Lift l i u1 u2 \to
30 \forall t1,t2. Lift l (succ i) t1 t2 \to
31 \forall r. Lift l i (intb r u1 t1) (intb r u2 t2)
32 | lift_flat : \forall i,u1,u2. Lift l i u1 u2 \to
33 \forall t1,t2. Lift l i t1 t2 \to
34 \forall r. Lift l i (intf r u1 t1) (intf r u2 t2)