no goals
α : Type u_1
β : Type ?u.39773
γ : Type ?u.39776
s t : Finset α
a b : α
hs : ¬a ∈ s
ht : ¬a ∈ t
⊢ cons a s hs ⊆ cons a t ht ↔ s ⊆ t
rwa [← coe_subset, coe_cons, coe_cons, Set.insert_subset_insert_iff, coe_subset]