contradiction
graph✝ : Graph
cls✝ : Class graph✝
child : Class.Child cls✝
path₁ : Path graph✝ (Class.Child.class child)
h✝ : prefix? (Path.cons child path₁) = none
h : ¬Option.isSome (prefix? (Path.cons child path₁)) = true
this : ¬Path.isCons (Path.cons child path₁) = true
⊢ ∃ path₂, Path.cons child path₁ ≻ path₂
no goals