constructor
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
⊢ prefix? path₁ = some path₂ ↔ prefix? (cons child path₁) = some (cons child path₂)
case mp
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
⊢ prefix? path₁ = some path₂ → prefix? (cons child path₁) = some (cons child path₂)

case mpr
graph : Graph
start : Class graph
child : Class.Child start
path₁ path₂ : Path graph (Class.Child.class child)
⊢ prefix? (cons child path₁) = some (cons child path₂) → prefix? path₁ = some path₂