∀ {α : Type u_1} {β : Type u_2} [inst : Membership α β] {p : Prop} [inst_1 : Decidable p] {a : α} {s : p → β}
  {t : ¬p → β}, (a ∈ if h : p then s h else t h) = ((∀ (h : p), a ∈ s h) ∧ ∀ (h : ¬p), a ∈ t h)