case intro.intro
α : Type u_1
β : Type ?u.516
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
a : ?m.551
h : a ∈ decode n
e : encode a = n
⊢ encode (ofNat α n) = n
α : Type u_1
β : Type ?u.516
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ encode (ofNat α n) = n
obtain ⟨a, h, e⟩ := decode_inv n
no goals
case intro.intro
α : Type u_1
β : Type ?u.516
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
a : ?m.551
h : a ∈ decode n
e : encode a = n
⊢ encode (ofNat α n) = n
rwa [ofNat_of_decode h]