no goals
ε : Type u_1
p : ε → Prop
inst✝ : DecidablePred p
ep ep' : Perm { a // p a }
en en' : Perm { a // ¬p a }
a : ε
⊢ ↑(subtypeCongr ep en) a = if h : p a then ↑(↑ep { val := a, property := h }) else ↑(↑en { val := a, property := h })
by_cases h : p a <;> simp [Perm.subtypeCongr, h]