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

State before:
α : Type u_1
x : α
xs : List α
⊢ [] ≠ x :: xs
Tactic:
intro h'
State after:
α : Type u_1
x : α
xs : List α
h' : [] = x :: xs
⊢ False

State before:
α : Type u_1
x : α
xs : List α
h' : [] = x :: xs
⊢ False
Tactic:
contradiction
State after:
no goals