simp [fintypeEquivFin]
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ fintypeEquivFin.symm 1 = true
ι : Type u_1
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Encodable ι
⊢ (sortedUniv Bool).get (cast ⋯ 1) = true