no goals
α : Type u
β : Type v
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : α → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
⊢ ↑sign (subtypeCongr ep en) = ↑sign ep * ↑sign en
simp [subtypeCongr]