case h.h.h
α : Type u_1
sep : α
l : List α
⊢ intersperse sep l = intersperseTR sep l
⊢ @intersperse = @intersperseTR
funext α sep l
case h.h.h
α : Type u_1
sep : α
l : List α
⊢ intersperse sep l =
    match l with
    | [] => []
    | [x] => [x]
    | x :: y :: xs => x :: sep :: y :: foldr (fun a r => sep :: a :: r) [] xs
case h.h.h
α : Type u_1
sep : α
l : List α
⊢ intersperse sep l = intersperseTR sep l
simp [intersperseTR]
no goals
case h.h.h
α : Type u_1
sep : α
l : List α
⊢ intersperse sep l =
    match l with
    | [] => []
    | [x] => [x]
    | x :: y :: xs => x :: sep :: y :: foldr (fun a r => sep :: a :: r) [] xs
match l with
| [] | [_] => rfl
| x::y::xs => simp [intersperse]; induction xs generalizing y <;> simp [*]
no goals
α : Type u_1
sep : α
l : List α
head✝ : α
⊢ intersperse sep [head✝] =
    match [head✝] with
    | [] => []
    | [x] => [x]
    | x :: y :: xs => x :: sep :: y :: foldr (fun a r => sep :: a :: r) [] xs
rfl
α : Type u_1
sep : α
l : List α
x y : α
xs : List α
⊢ intersperse sep (y :: xs) = y :: foldr (fun a r => sep :: a :: r) [] xs
α : Type u_1
sep : α
l : List α
x y : α
xs : List α
⊢ intersperse sep (x :: y :: xs) =
    match x :: y :: xs with
    | [] => []
    | [x] => [x]
    | x :: y :: xs => x :: sep :: y :: foldr (fun a r => sep :: a :: r) [] xs
simp [intersperse]
no goals
α : Type u_1
sep : α
l : List α
x y : α
xs : List α
⊢ intersperse sep (y :: xs) = y :: foldr (fun a r => sep :: a :: r) [] xs
induction xs generalizing y <;> simp [*]