∀ {α : Type u_1} [inst : Denumerable α] (s : Finset α),
  ((fun n =>
          Finset.map (Denumerable.eqv α).symm.toEmbedding (Denumerable.raise'Finset (Denumerable.ofNat (List ℕ) n) 0))
        ((fun s =>
            Encodable.encode
              (Denumerable.lower' ((Finset.map (Denumerable.eqv α).toEmbedding s).sort fun a b => a ≤ b) 0))
          s)).val =
    s.val