[changelog]: Data.Bool.Properties.if-idem

Author: pmbittner

CHANGELOG.md

@@ -242,6 +242,7 @@ Additions to existing modules
 * In `Data.Bool.Properties`:
   ```agda
   if-eta : ∀ b → (if b then x else x) ≡ x
+  if-idem : ∀ b → (if b then (if b then x else y) else y) ≡ (if b then x else y)
   if-swap-then : ∀ b c → (if b then (if c then x else y) else y) ≡ (if c then (if b then x else y) else y)
   if-swap-else : ∀ b c → (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y))
   if-not : ∀ b → (if not b then x else y) ≡ (if b then y else x)