no goals
α : Type u
inst✝⁵ : Primcodable α
inst✝⁴ : Inhabited α
β : Type v
inst✝³ : Primcodable β
inst✝² : Inhabited β
γ : Type w
inst✝¹ : Primcodable γ
inst✝ : Inhabited γ
p : Set α
q : Set β
⊢ ManyOneEquiv (toNat p) (toNat q) ↔ ManyOneEquiv p q
simp [ManyOneEquiv]