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

State before:
α : Type
x y : α
xs ys : List α
h : x :: xs = y :: ys
⊢ x = y ∧ xs = ys
Tactic:
cases h
State after:
case refl
α : Type
x : α
xs : List α
⊢ x = x ∧ xs = xs

State before:
case refl
α : Type
x : α
xs : List α
⊢ x = x ∧ xs = xs
Tactic:
simp
State after:
no goals