no goals
α : Type u
β : Type v
γ : Type w
as bs : List α
a b : α
h : concat as a = concat bs b
⊢ as = bs ∧ a = b
match as, bs with
| [], [] => simp [concat] at h; simp [h]
| [_], [] => simp [concat] at h
| _::_::_, [] => simp [concat] at h
| [], [_] => simp [concat] at h
| [], _::_::_ => simp [concat] at h
| _::_, _::_ => simp [concat] at h; simp [h]; apply of_concat_eq_concat h.2
α : Type u
β : Type v
γ : Type w
as bs : List α
a b : α
h : a = b
⊢ nil = nil ∧ a = b
α : Type u
β : Type v
γ : Type w
as bs : List α
a b : α
h : concat nil a = concat nil b
⊢ nil = nil ∧ a = b
simp [concat] at h
no goals
α : Type u
β : Type v
γ : Type w
as bs : List α
a b : α
h : a = b
⊢ nil = nil ∧ a = b
simp [h]
no goals
α : Type u
β : Type v
γ : Type w
as bs : List α
a b head✝ : α
h : concat (head✝ :: nil) a = concat nil b
⊢ head✝ :: nil = nil ∧ a = b
simp [concat] at h
no goals
α : Type u
β : Type v
γ : Type w
as bs : List α
a b head✝¹ head✝ : α
tail✝ : List α
h : concat (head✝¹ :: head✝ :: tail✝) a = concat nil b
⊢ head✝¹ :: head✝ :: tail✝ = nil ∧ a = b
simp [concat] at h
no goals
α : Type u
β : Type v
γ : Type w
as bs : List α
a b head✝ : α
h : concat nil a = concat (head✝ :: nil) b
⊢ nil = head✝ :: nil ∧ a = b
simp [concat] at h
no goals
α : Type u
β : Type v
γ : Type w
as bs : List α
a b head✝¹ head✝ : α
tail✝ : List α
h : concat nil a = concat (head✝¹ :: head✝ :: tail✝) b
⊢ nil = head✝¹ :: head✝ :: tail✝ ∧ a = b
simp [concat] at h
α : Type u
β : Type v
γ : Type w
as bs : List α
a b head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
h : head✝¹ = head✝ ∧ concat tail✝¹ a = concat tail✝ b
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝ ∧ a = b
α : Type u
β : Type v
γ : Type w
as bs : List α
a b head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
h : concat (head✝¹ :: tail✝¹) a = concat (head✝ :: tail✝) b
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝ ∧ a = b
simp [concat] at h
α : Type u
β : Type v
γ : Type w
as bs : List α
a b head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
h : head✝¹ = head✝ ∧ concat tail✝¹ a = concat tail✝ b
⊢ tail✝¹ = tail✝ ∧ a = b
α : Type u
β : Type v
γ : Type w
as bs : List α
a b head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
h : head✝¹ = head✝ ∧ concat tail✝¹ a = concat tail✝ b
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝ ∧ a = b
simp [h]
no goals
α : Type u
β : Type v
γ : Type w
as bs : List α
a b head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
h : head✝¹ = head✝ ∧ concat tail✝¹ a = concat tail✝ b
⊢ tail✝¹ = tail✝ ∧ a = b
apply of_concat_eq_concat h.2