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 include "Basic_2/substitution/lift_vector.ma".
17 (* GENERIC RELOCATION *******************************************************)
19 inductive lifts: list2 nat nat → relation term ≝
20 | lifts_nil : ∀T. lifts ⟠ T T
21 | lifts_cons: ∀T1,T,T2,des,d,e.
22 ⇑[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} :: des) T1 T2
25 interpretation "generic relocation" 'RLift des T1 T2 = (lifts des T1 T2).