proof on recursive step

module Hanoi

import Data.Vect

data Peg
    = First
    | Second
    | Third

-- TODO : can we do better here?
Eq Peg where
    First == First = True
    Second == Second = True
    Third == Third = True
    _ == _ = False

Disposition : Nat -> Type
Disposition diskNumber = Vect diskNumber Peg

startingDisposition : (diskNumber: Nat) -> Disposition diskNumber
startingDisposition diskNumber = replicate diskNumber First

data So : Bool -> Type where
    Oh : So True
    
tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber)
tryMove Z from to [] = Nothing
tryMove (S k) from to (smallestDiskPosition :: restOfTheDisposition) =
        map (smallestDiskPosition ::) (tryMove k from to restOfTheDisposition)

You can import Data.So instead of defining your own version of it