no goals
α : Type u_1
as bs cs : List α
h : as ++ bs = as ++ cs
⊢ bs = cs
induction as with
| nil => assumption
| cons a as ih =>
  injection h with _ h
  exact ih h
no goals
case nil
α : Type u_1
bs cs : List α
h : [] ++ bs = [] ++ cs
⊢ bs = cs
assumption
case cons
α : Type u_1
bs cs : List α
a : α
as : List α
ih : as ++ bs = as ++ cs → bs = cs
head_eq✝ : a = a
h : List.append as bs = List.append as cs
⊢ bs = cs
case cons
α : Type u_1
bs cs : List α
a : α
as : List α
ih : as ++ bs = as ++ cs → bs = cs
h : a :: as ++ bs = a :: as ++ cs
⊢ bs = cs
injection h with _ h
no goals
case cons
α : Type u_1
bs cs : List α
a : α
as : List α
ih : as ++ bs = as ++ cs → bs = cs
head_eq✝ : a = a
h : List.append as bs = List.append as cs
⊢ bs = cs
exact ih h