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