case mpr
α : Type u
l l' : List α
h : l ~r reverse l'
⊢ reverse l ~r l'
case mpr
α : Type u
l l' : List α
⊢ l ~r reverse l' → reverse l ~r l'
intro h
no goals
case mpr
α : Type u
l l' : List α
h : l ~r reverse l'
⊢ reverse l ~r l'
simpa using h.reverse