apply And.intro <;> intros _ <;> apply Hne
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
⊢ x ≠ a ∧ ¬x ∈ as
case left
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
a✝ : x = a
⊢ x ∈ a :: as

case right
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
a✝ : x ∈ as
⊢ x ∈ a :: as