no goals
α : Type u_1
β : Type ?u.668395
inst✝ : DecidableEq α
l : List α
x✝ x y : α
xs : List α
h : Nodup (x :: y :: xs)
⊢ ↑(formPerm (x :: y :: xs)) x = y
simp [formPerm_apply_of_not_mem _ _ h.not_mem]