module LongProof3 where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

{-# BUILTIN NATURAL Nat #-}

data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A

infixr 40 _::_

_++_ : {A : Set} -> List A -> List A -> List A
_++_ [] b = b
_++_ (a :: as) b = a :: (as ++ b)

appx : ∀ {A} → Nat → List A → List A
appx zero _ = []
appx (suc x) a = a ++ (appx x a)

length : { A : Set } -> List A -> Nat
length [] = zero
length (_ :: as) = suc (length as)

data _==_ { A : Set} (x : A) : A -> Set where
  refl : x == x

y : Nat
y = (length (appx 50000 (1 :: 2 :: 3 :: [])))

v : (z : Nat) → (length (appx z (1 :: 2 :: 3 :: []))) == 150000 → Nat
v z eq = zero

-- stack overflow
w : Nat
w = v 50000 (refl {x = 150000})