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

Author: pmbittner

src/Data/Bool/Properties.agda

@@ -750,6 +750,11 @@ if-eta : ∀ b {x : A} →
 if-eta false = refl
 if-eta true  = refl
 
+if-idem : ∀ b {x y : A} →
+          (if b then (if b then x else y) else y) ≡ (if b then x else y)
+if-idem false = refl
+if-idem true  = refl
+
 if-swap-then : ∀ b c {x y : A} →
           (if b then (if c then x else y) else y)
         ≡ (if c then (if b then x else y) else y)