constructor
graph : Graph
start : Class graph
path : Path graph start
⊢ Option.isSome (prefix? path) = true ↔ isCons path = true
case mp
graph : Graph
start : Class graph
path : Path graph start
⊢ Option.isSome (prefix? path) = true → isCons path = true

case mpr
graph : Graph
start : Class graph
path : Path graph start
⊢ isCons path = true → Option.isSome (prefix? path) = true