Theorem: LoVe.cases_Eq_example (LoVe/Lectures/LoVe06_InductivePredicates_Demo.lean)

State before:
α : Type
l r : α
h : l = r
P : α → α → Prop
⊢ P l r
Tactic:
cases h
State after:
case refl
α : Type
l : α
P : α → α → Prop
⊢ P l l

State before:
case refl
α : Type
l : α
P : α → α → Prop
⊢ P l l
Tactic:
sorry
State after:
no goals