case nil
α : Type u_1
β : Type ?u.665997
inst✝ : DecidableEq α
l : List α
x✝¹ x✝ y✝ x y : α
⊢ ↑(formPerm (x :: ([] ++ [y]))) y = x

case cons
α : Type u_1
β : Type ?u.665997
inst✝ : DecidableEq α
l : List α
x✝¹ x✝ y✝ z : α
xs : List α
IH : ∀ (x y : α), ↑(formPerm (x :: (xs ++ [y]))) y = x
x y : α
⊢ ↑(formPerm (x :: (z :: xs ++ [y]))) y = x
α : Type u_1
β : Type ?u.665997
inst✝ : DecidableEq α
l : List α
x✝ x y : α
xs : List α
⊢ ↑(formPerm (x :: (xs ++ [y]))) y = x
induction' xs with z xs IH generalizing x y
no goals
case nil
α : Type u_1
β : Type ?u.665997
inst✝ : DecidableEq α
l : List α
x✝¹ x✝ y✝ x y : α
⊢ ↑(formPerm (x :: ([] ++ [y]))) y = x
simp
no goals
case cons
α : Type u_1
β : Type ?u.665997
inst✝ : DecidableEq α
l : List α
x✝¹ x✝ y✝ z : α
xs : List α
IH : ∀ (x y : α), ↑(formPerm (x :: (xs ++ [y]))) y = x
x y : α
⊢ ↑(formPerm (x :: (z :: xs ++ [y]))) y = x
simp [IH]