Theorem: list_cons_ne_nil (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