α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
H : toList p x = [y]
⊢ False
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
⊢ toList p x ≠ [y]
intro H
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x y : α
H : toList p x = [y]
⊢ False
simpa [card_support_ne_one] using congr_arg length H