no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
l₁ l₂ : List (List α)
h : l₁ ~ l₂
x₁ x₂ : List α
xs : List (List α)
⊢ List.join (x₂ :: x₁ :: xs) ~ List.join (x₁ :: x₂ :: xs)
simpa only [join, append_assoc] using perm_append_comm.append_right _