Theorem: Collection.set_cons (Logic/Vorspiel/Collection.lean)

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

State before:
case h
β : Type u_1
α : Type u_2
inst✝ : Collection β α
z : β
a : α
x✝ : β
⊢ x✝ ∈ set (cons z a) ↔ x✝ ∈ insert z (set a)
Tactic:
simp [set]
State after:
no goals