Theorem: HMem.Complexity.Karatsuba.eq_decide (HMem/Complexity/BitTree.lean)

State before:
P : Prop
b : Bool
inst✝ : Decidable P
⊢ (b = decide P) = (decide (b = true) = true ↔ P)
Tactic:
cases b <;> simp
State after:
no goals