-- 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