α : Type u_1
l₁ l₂ : List α
a : α
s : l₁ ⊆ l₂
x✝ : α
⊢ x✝ = a ∨ x✝ ∈ l₁ → x✝ = a ∨ x✝ ∈ l₂
α : Type u_1
l₁ l₂ : List α
a : α
s : l₁ ⊆ l₂
x✝ : α
⊢ x✝ ∈ a :: l₁ → x✝ ∈ a :: l₂
simp only [mem_cons]
no goals
α : Type u_1
l₁ l₂ : List α
a : α
s : l₁ ⊆ l₂
x✝ : α
⊢ x✝ = a ∨ x✝ ∈ l₁ → x✝ = a ∨ x✝ ∈ l₂
exact Or.imp_right (@s _)