(* GENERIC RELOCATION WITH PAIRS ********************************************)
inductive minuss: nat → relation (list2 nat nat) ≝
| minuss_nil: ∀i. minuss i ⟠ ⟠
| minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 →
(* GENERIC RELOCATION WITH PAIRS ********************************************)
inductive minuss: nat → relation (list2 nat nat) ≝
| minuss_nil: ∀i. minuss i ⟠ ⟠
| minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 →