Theorem: list_nil_ne_app_cons (Katydid/Std/Lists.lean)

State before:
α : Type u_1
y : α
xs ys : List α
⊢ [] ≠ xs ++ y :: ys
Tactic:
cases xs <;> { intro h' ; contradiction }
State after:
no goals

State before:
case cons
α : Type u_1
y : α
ys : List α
head✝ : α
tail✝ : List α
⊢ [] ≠ head✝ :: tail✝ ++ y :: ys
Tactic:
intro h'
State after:
case cons
α : Type u_1
y : α
ys : List α
head✝ : α
tail✝ : List α
h' : [] = head✝ :: tail✝ ++ y :: ys
⊢ False

State before:
case cons
α : Type u_1
y : α
ys : List α
head✝ : α
tail✝ : List α
h' : [] = head✝ :: tail✝ ++ y :: ys
⊢ False
Tactic:
contradiction
State after:
no goals