case nil
α : Type u_1
β : Type ?u.4805
γ : Type ?u.4808
x : SingleObj α
⊢ listToPath (pathToList Path.nil) = Path.cast (_ : star α = star α) (_ : star α = star α) Path.nil

case cons
α : Type u_1
β : Type ?u.4805
γ : Type ?u.4808
x y z : SingleObj α
p : Path (star α) y
a : y ⟶ z
ih : listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : y = star α) p
⊢ listToPath (pathToList (Path.cons p a)) = Path.cast (_ : star α = star α) (_ : z = star α) (Path.cons p a)
α : Type u_1
β : Type ?u.4805
γ : Type ?u.4808
x : SingleObj α
p : Path (star α) x
⊢ listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : x = star α) p
induction' p with y z p a ih
no goals
case nil
α : Type u_1
β : Type ?u.4805
γ : Type ?u.4808
x : SingleObj α
⊢ listToPath (pathToList Path.nil) = Path.cast (_ : star α = star α) (_ : star α = star α) Path.nil
rfl
case cons
α : Type u_1
β : Type ?u.4805
γ : Type ?u.4808
x y z : SingleObj α
p : Path (star α) y
a : y ⟶ z
ih : listToPath (pathToList p) = p
⊢ Path.cons (listToPath (pathToList p)) a = Path.cons p a
case cons
α : Type u_1
β : Type ?u.4805
γ : Type ?u.4808
x y z : SingleObj α
p : Path (star α) y
a : y ⟶ z
ih : listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : y = star α) p
⊢ listToPath (pathToList (Path.cons p a)) = Path.cast (_ : star α = star α) (_ : z = star α) (Path.cons p a)
dsimp at *
no goals
case cons
α : Type u_1
β : Type ?u.4805
γ : Type ?u.4808
x y z : SingleObj α
p : Path (star α) y
a : y ⟶ z
ih : listToPath (pathToList p) = p
⊢ Path.cons (listToPath (pathToList p)) a = Path.cons p a
rw [ih]