constructor
case a
α : Sort u_1
a : α
s : Set α
x : α
⊢ x ∈ s.insertIf a True ↔ x ∈ s.insert a
case a.mp
α : Sort u_1
a : α
s : Set α
x : α
⊢ x ∈ s.insertIf a True → x ∈ s.insert a

case a.mpr
α : Sort u_1
a : α
s : Set α
x : α
⊢ x ∈ s.insert a → x ∈ s.insertIf a True