all_goals
  intro h
  cases path₁
  case nil => simp [prefix?] at h
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₂
case mp.cons
graph : Graph
start : Class graph
child : Class.Child start
path₂ : Path graph (Class.Child.class child)
child✝ : Class.Child (Class.Child.class child)
a✝ : Path graph (Class.Child.class child✝)
h : prefix? (cons child✝ a✝) = some path₂
⊢ prefix? (cons child (cons child✝ a✝)) = some (cons child path₂)

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