Theorem: LoVe.distinctness_example (LoVe/Lectures/LoVe05_FunctionalProgramming_Demo.lean)

State before:
α : Type
y : α
ys : List α
h : [] = y :: ys
⊢ false = true
Tactic:
cases h
State after:
no goals