case nil
α : Type u_1
β : Type ?u.5108
γ : Type ?u.5111
⊢ pathToList (listToPath []) = []

case cons
α : Type u_1
β : Type ?u.5108
γ : Type ?u.5111
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ pathToList (listToPath (a :: l)) = a :: l
α : Type u_1
β : Type ?u.5108
γ : Type ?u.5111
l : List α
⊢ pathToList (listToPath l) = l
induction' l with a l ih
no goals
case nil
α : Type u_1
β : Type ?u.5108
γ : Type ?u.5111
⊢ pathToList (listToPath []) = []
rfl
case cons
α : Type u_1
β : Type ?u.5108
γ : Type ?u.5111
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ a :: pathToList (listToPath l) = a :: l
case cons
α : Type u_1
β : Type ?u.5108
γ : Type ?u.5111
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ pathToList (listToPath (a :: l)) = a :: l
change a :: pathToList (listToPath l) = a :: l
no goals
case cons
α : Type u_1
β : Type ?u.5108
γ : Type ?u.5111
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ a :: pathToList (listToPath l) = a :: l
rw [ih]