-- after push 1 and 2, pop2 get 1 and 2

testStack02 : {m : Level } !$\rightarrow$!  ( Stack  !$\mathbb{N}$! (SingleLinkedStack !$\mathbb{N}$!) !$\rightarrow$! Bool {m} ) !$\rightarrow$! Bool {m}
testStack02 cs = pushStack createSingleLinkedStack 1 (\s !$\rightarrow$! pushStack s 2 cs)


testStack031 : (d1 d2 : !$\mathbb{N}$! ) !$\rightarrow$! Bool {Zero}
testStack031 2 1 = True
testStack031 _ _ = False

testStack032 : (d1 d2 : Maybe !$\mathbb{N}$!) !$\rightarrow$! Bool {Zero}
testStack032  (Just d1) (Just d2) = testStack031 d1 d2
testStack032  _ _ = False

testStack03 : {m : Level } !$\rightarrow$! Stack  !$\mathbb{N}$! (SingleLinkedStack !$\mathbb{N}$!) !$\rightarrow$! ((Maybe !$\mathbb{N}$!) !$\rightarrow$! (Maybe !$\mathbb{N}$!) !$\rightarrow$! Bool {m} ) !$\rightarrow$! Bool {m}
testStack03 s cs = pop2Stack s (\s d1 d2 !$\rightarrow$! cs d1 d2 )

testStack04 : Bool
testStack04 = testStack02 (\s !$\rightarrow$! testStack03 s testStack032)

testStack05 : testStack04 !$\equiv$! True
testStack05 = refl