intro h
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
⊢ cons c₁ (cons c₂ path₁) ≻ path₂ → Path.isCons path₂ = true
graph✝ : Graph
cls✝ : Class graph✝
c₁ : Class.Child cls✝
c₂ : Class.Child (Class.Child.class c₁)
path₁ : Path graph✝ (Class.Child.class c₂)
path₂ : Path graph✝ cls✝
h : cons c₁ (cons c₂ path₁) ≻ path₂
⊢ Path.isCons path₂ = true