working.idr

 -- GOAL: push values of type Either a b to a Stack and maintain a type-level                                                                                                   
 -- count of Left (n) and Right (m) cases
 data Stack a b = MkStack (n : Nat ** (m : Nat ** Vect (n + m) (Either a b)))

 push : Either a b -> Stack a b -> Stack a b
 push (Left l)  (MkStack (n ** (m ** v))) = MkStack ((S n) ** (m     ** (Left l  :: v)))
 push (Right r) (MkStack (n ** (m ** v))) = MkStack (n     ** ((S m) ** v'))
   where v' : Vect (n + S (m)) (Either a b)
         v' = rewrite (sym $ plusSuccRightSucc n m) in Right r :: v