α : Type u
β : Type v
γ : Type w
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
⊢ ∀ (b : α) (s' : Seq α), a = b ∨ a ∈ append s' s₂ → a ∈ append (cons b s') s₂
α : Type u
β : Type v
γ : Type w
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
⊢ a ∈ append s₁ s₂
apply mem_rec_on h
α : Type u
β : Type v
γ : Type w
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
b✝ : α
s'✝ : Seq α
a✝ : a = b✝ ∨ a ∈ append s'✝ s₂
⊢ a ∈ append (cons b✝ s'✝) s₂
α : Type u
β : Type v
γ : Type w
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
⊢ ∀ (b : α) (s' : Seq α), a = b ∨ a ∈ append s' s₂ → a ∈ append (cons b s') s₂
intros
no goals
α : Type u
β : Type v
γ : Type w
s₁ s₂ : Seq α
a : α
h : a ∈ s₁
b✝ : α
s'✝ : Seq α
a✝ : a = b✝ ∨ a ∈ append s'✝ s₂
⊢ a ∈ append (cons b✝ s'✝) s₂
simp [*]