no goals
α : Type u_1
β : Type ?u.671041
inst✝ : DecidableEq α
l : List α
x✝ x y : α
⊢ ↑(formPerm (y :: l)) x = y ↔ ↑(formPerm (y :: l)) x = ↑(formPerm (y :: l)) (getLast (y :: l) (_ : y :: l ≠ []))
rw [formPerm_apply_getLast]