theorem Finset.coe_subset_singleton {α : Type u_1} {s : Finset α} {a : α} : ↑s ⊆ {a} ↔ s ⊆ {a}

theorem Finset.singleton_subset_coe {α : Type u_1} {s : Finset α} {a : α} : {a} ⊆ ↑s ↔ {a} ⊆ s