α : Type u
β : Type v
γ : Type w
a : α
as bs : List α
h : a ∈ as
⊢ a ∈ as ++ bs
α : Type u
β : Type v
γ : Type w
a : α
as bs : List α
⊢ a ∈ as → a ∈ as ++ bs
intro h
no goals
α : Type u
β : Type v
γ : Type w
a : α
as bs : List α
h : a ∈ as
⊢ a ∈ as ++ bs
induction h with
| head => apply Mem.head
| tail => apply Mem.tail; assumption
no goals
case head
α : Type u
β : Type v
γ : Type w
a : α
as bs as✝ : List α
⊢ a ∈ a :: as✝ ++ bs
apply Mem.head
case tail.a
α : Type u
β : Type v
γ : Type w
a : α
as bs : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
a_ih✝ : a ∈ as✝ ++ bs
⊢ Mem a (List.append as✝ bs)
case tail
α : Type u
β : Type v
γ : Type w
a : α
as bs : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
a_ih✝ : a ∈ as✝ ++ bs
⊢ a ∈ b✝ :: as✝ ++ bs
apply Mem.tail
no goals
case tail.a
α : Type u
β : Type v
γ : Type w
a : α
as bs : List α
b✝ : α
as✝ : List α
a✝ : Mem a as✝
a_ih✝ : a ∈ as✝ ++ bs
⊢ Mem a (List.append as✝ bs)
assumption