Theorem: Bool.apply_cond (Controlbits/Bool.lean)

State before:
α : Type u_1
β : Type u_2
f : α → β
b : Bool
x y : α
⊢ f (bif b then x else y) = bif b then f x else f y
Tactic:
cases b <;> rfl
State after:
no goals