case refine_1
α✝ : Type u_1
l₁ l₂ : List α✝
x✝ : reverse l₁ <:+: reverse l₂
s t : List α✝
e : s ++ reverse l₁ ++ t = reverse l₂
⊢ reverse t ++ l₁ ++ reverse s = l₂

case refine_2
α✝ : Type u_1
l₁ l₂ : List α✝
x✝ : l₁ <:+: l₂
s t : List α✝
e : s ++ l₁ ++ t = l₂
⊢ reverse t ++ reverse l₁ ++ reverse s = reverse l₂
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ reverse l₁ <:+: reverse l₂ ↔ l₁ <:+: l₂
refine ⟨fun ⟨s, t, e⟩ => ⟨reverse t, reverse s, ?_⟩, fun ⟨s, t, e⟩ => ⟨reverse t, reverse s, ?_⟩⟩
no goals
case refine_1
α✝ : Type u_1
l₁ l₂ : List α✝
x✝ : reverse l₁ <:+: reverse l₂
s t : List α✝
e : s ++ reverse l₁ ++ t = reverse l₂
⊢ reverse t ++ l₁ ++ reverse s = l₂
rw [← reverse_reverse l₁, append_assoc, ← reverse_append, ← reverse_append, e,
  reverse_reverse]
no goals
case refine_2
α✝ : Type u_1
l₁ l₂ : List α✝
x✝ : l₁ <:+: l₂
s t : List α✝
e : s ++ l₁ ++ t = l₂
⊢ reverse t ++ reverse l₁ ++ reverse s = reverse l₂
rw [append_assoc, ← reverse_append, ← reverse_append, e]