ext
β : Type u_1
α : Type u_2
inst✝ : Collection β α
z : β
a : α
⊢ set (cons z a) = insert z (set a)
case h
β : Type u_1
α : Type u_2
inst✝ : Collection β α
z : β
a : α
x✝ : β
⊢ x✝ ∈ set (cons z a) ↔ x✝ ∈ insert z (set a)