error.idris

module Main

import Data.Nat

data Stack_ : Nat -> Type -> Type where
  Two : (1 _ : Stack_ (2 * i) a) -> Stack_ i a

data Debits_ : Nat -> Stack_ i a -> Type where
  DTwo : (1 _ : Debits_ (i + acc) s) -> Debits_ acc (Two s)

draise_ : LTE acc acc' -> (1 _ : Debits_ {i} {a} acc s) -> Debits_ {i} acc' s
draise_ n (DTwo s) = DTwo (draise_ m s) where
  m : LTE (i + acc) (i + acc')