inductive minuss: nat → relation mr2 ≝
| minuss_nil: ∀i. minuss i (◊) (◊)
| minuss_lt : ∀cs1,cs2,l,m,i. i < l → minuss i cs1 cs2 →
inductive minuss: nat → relation mr2 ≝
| minuss_nil: ∀i. minuss i (◊) (◊)
| minuss_lt : ∀cs1,cs2,l,m,i. i < l → minuss i cs1 cs2 →