Theorem: Misc.dite_eq_left_iff (LeanSAT/Util/Misc.lean)

State before:
P : Prop
α✝ : Sort u_1
a : α✝
B : ¬P → α✝
inst✝ : Decidable P
⊢ dite P (fun x => a) B = a ↔ ∀ (h : ¬P), B h = a
Tactic:
by_cases P <;> simp [*, forall_prop_of_true, forall_prop_of_false]
State after:
no goals