diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 1a3e105604..446a82d868 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -19,9 +19,7 @@ open import Relation.Binary.Definitions using (Reflexive)
 module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
 
   sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_
-  sel⇒idem sel x with sel x x
-  ... | inj₁ x•x≈x = x•x≈x
-  ... | inj₂ x•x≈x = x•x≈x
+  sel⇒idem sel x = reduce (sel x x)
 
 module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
 
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index e9ddbe6387..d4008fce07 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -130,15 +130,15 @@ module _ (f : A → Maybe B) where
 
   mapMaybe-concatMap : mapMaybe f ≗ concatMap (fromMaybe ∘ f)
   mapMaybe-concatMap [] = refl
-  mapMaybe-concatMap (x ∷ xs) with f x
-  ... | just y  = cong (y ∷_) (mapMaybe-concatMap xs)
-  ... | nothing = mapMaybe-concatMap xs
+  mapMaybe-concatMap (x ∷ xs) with ih ← mapMaybe-concatMap xs | f x
+  ... | just y  = cong (y ∷_) ih
+  ... | nothing = ih
 
   length-mapMaybe : ∀ xs → length (mapMaybe f xs) ≤ length xs
   length-mapMaybe []       = z≤n
-  length-mapMaybe (x ∷ xs) with f x
-  ... | just y  = s≤s (length-mapMaybe xs)
-  ... | nothing = m≤n⇒m≤1+n (length-mapMaybe xs)
+  length-mapMaybe (x ∷ xs) with ih ← length-mapMaybe xs | f x
+  ... | just y  = s≤s ih
+  ... | nothing = m≤n⇒m≤1+n ih
 
 ------------------------------------------------------------------------
 -- _++_
@@ -497,8 +497,8 @@ module _ {P : Pred A p} {f : A → A → A} where
   foldr-forcesᵇ : (∀ x y → P (f x y) → P x × P y) →
                   ∀ e xs → P (foldr f e xs) → All P xs
   foldr-forcesᵇ _      _ []       _     = []
-  foldr-forcesᵇ forces _ (x ∷ xs) Pfold with forces _ _ Pfold
-  ... | (px , pfxs) = px ∷ foldr-forcesᵇ forces _ xs pfxs
+  foldr-forcesᵇ forces _ (x ∷ xs) Pfold =
+    let px , pfxs = forces _ _ Pfold in px ∷ foldr-forcesᵇ forces _ xs pfxs
 
   foldr-preservesᵇ : (∀ {x y} → P x → P y → P (f x y)) →
                      ∀ {e xs} → P e → All P xs → P (foldr f e xs)
@@ -627,11 +627,10 @@ scanr-defn : ∀ (f : A → B → B) (e : B) →
              scanr f e ≗ map (foldr f e) ∘ tails
 scanr-defn f e []             = refl
 scanr-defn f e (x ∷ [])       = refl
-scanr-defn f e (x ∷ y ∷ xs)
-  with scanr f e (y ∷ xs) | scanr-defn f e (y ∷ xs)
-... | []     | ()
-... | z ∷ zs | eq with ∷-injective eq
-...   | z≡fy⦇f⦈xs , _ = cong₂ (λ z → f x z ∷_) z≡fy⦇f⦈xs eq
+scanr-defn f e (x ∷ y∷xs@(_ ∷ _))
+  with eq ← scanr-defn f e y∷xs
+  with z ∷ zs ← scanr f e y∷xs
+  = let z≡fy⦇f⦈xs , _ = ∷-injective eq in cong₂ (λ z → f x z ∷_) z≡fy⦇f⦈xs eq
 
 ------------------------------------------------------------------------
 -- scanl
@@ -778,8 +777,7 @@ take++drop (suc n) (x ∷ xs) = cong (x ∷_) (take++drop n xs)
 splitAt-defn : ∀ n → splitAt {A = A} n ≗ < take n , drop n >
 splitAt-defn zero    xs       = refl
 splitAt-defn (suc n) []       = refl
-splitAt-defn (suc n) (x ∷ xs) with splitAt n xs | splitAt-defn n xs
-... | (ys , zs) | ih = cong (Prod.map (x ∷_) id) ih
+splitAt-defn (suc n) (x ∷ xs) = cong (Prod.map (x ∷_) id) (splitAt-defn n xs)
 
 ------------------------------------------------------------------------
 -- takeWhile, dropWhile, and span
@@ -805,9 +803,9 @@ module _ {P : Pred A p} (P? : Decidable P) where
 
   length-filter : ∀ xs → length (filter P? xs) ≤ length xs
   length-filter []       = z≤n
-  length-filter (x ∷ xs) with does (P? x)
-  ... | false = m≤n⇒m≤1+n (length-filter xs)
-  ... | true  = s≤s (length-filter xs)
+  length-filter (x ∷ xs) with ih ← length-filter xs | does (P? x)
+  ... | false = m≤n⇒m≤1+n ih
+  ... | true  = s≤s ih
 
   filter-all : ∀ {xs} → All P xs → filter P? xs ≡ xs
   filter-all {[]}     []         = refl
@@ -819,9 +817,9 @@ module _ {P : Pred A p} (P? : Decidable P) where
   filter-notAll (x ∷ xs) (here ¬px) with P? x
   ... | false because _ = s≤s (length-filter xs)
   ... | yes          px = contradiction px ¬px
-  filter-notAll (x ∷ xs) (there any) with does (P? x)
-  ... | false = m≤n⇒m≤1+n (filter-notAll xs any)
-  ... | true  = s≤s (filter-notAll xs any)
+  filter-notAll (x ∷ xs) (there any) with ih ← filter-notAll xs any | does (P? x)
+  ... | false = m≤n⇒m≤1+n ih
+  ... | true  = s≤s ih
 
   filter-some : ∀ {xs} → Any P xs → 0 < length (filter P? xs)
   filter-some {x ∷ xs} (here px)   with P? x
@@ -862,9 +860,9 @@ module _ {P : Pred A p} (P? : Decidable P) where
 
   filter-++ : ∀ xs ys → filter P? (xs ++ ys) ≡ filter P? xs ++ filter P? ys
   filter-++ []       ys = refl
-  filter-++ (x ∷ xs) ys with does (P? x)
-  ... | true  = cong (x ∷_) (filter-++ xs ys)
-  ... | false = filter-++ xs ys
+  filter-++ (x ∷ xs) ys with ih ← filter-++ xs ys | does (P? x)
+  ... | true  = cong (x ∷_) ih
+  ... | false = ih
 
 ------------------------------------------------------------------------
 -- derun and deduplicate
@@ -874,9 +872,9 @@ module _ {R : Rel A p} (R? : B.Decidable R) where
   length-derun : ∀ xs → length (derun R? xs) ≤ length xs
   length-derun [] = ≤-refl
   length-derun (x ∷ []) = ≤-refl
-  length-derun (x ∷ y ∷ xs) with does (R? x y) | length-derun (y ∷ xs)
-  ... | true  | r = m≤n⇒m≤1+n r
-  ... | false | r = s≤s r
+  length-derun (x ∷ y ∷ xs) with ih ← length-derun (y ∷ xs) | does (R? x y) 
+  ... | true  = m≤n⇒m≤1+n ih
+  ... | false = s≤s ih
 
   length-deduplicate : ∀ xs → length (deduplicate R? xs) ≤ length xs
   length-deduplicate [] = z≤n
@@ -905,16 +903,16 @@ module _ {P : Pred A p} (P? : Decidable P) where
 
   partition-defn : partition P? ≗ < filter P? , filter (∁? P?) >
   partition-defn []       = refl
-  partition-defn (x ∷ xs) with does (P? x)
-  ...  | true  = cong (Prod.map (x ∷_) id) (partition-defn xs)
-  ...  | false = cong (Prod.map id (x ∷_)) (partition-defn xs)
+  partition-defn (x ∷ xs) with ih ← partition-defn xs | does (P? x)
+  ...  | true  = cong (Prod.map (x ∷_) id) ih
+  ...  | false = cong (Prod.map id (x ∷_)) ih
 
   length-partition : ∀ xs → (let (ys , zs) = partition P? xs) →
                      length ys ≤ length xs × length zs ≤ length xs
   length-partition []       = z≤n , z≤n
-  length-partition (x ∷ xs) with does (P? x) | length-partition xs
-  ...  | true  | rec = Prod.map s≤s m≤n⇒m≤1+n rec
-  ...  | false | rec = Prod.map m≤n⇒m≤1+n s≤s rec
+  length-partition (x ∷ xs) with ih ← length-partition xs | does (P? x)
+  ...  | true  = Prod.map s≤s m≤n⇒m≤1+n ih
+  ...  | false = Prod.map m≤n⇒m≤1+n s≤s ih
 
 ------------------------------------------------------------------------
 -- _ʳ++_
@@ -1063,8 +1061,8 @@ module _ {x y : A} where
 
   ∷ʳ-injective : ∀ xs ys → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
   ∷ʳ-injective []          []          refl = (refl , refl)
-  ∷ʳ-injective (x ∷ xs)    (y  ∷ ys)   eq   with ∷-injective eq
-  ... | refl , eq′ = Prod.map (cong (x ∷_)) id (∷ʳ-injective xs ys eq′)
+  ∷ʳ-injective (x ∷ xs)    (y  ∷ ys)   eq   with refl , eq′  ← ∷-injective eq
+    = Prod.map (cong (x ∷_)) id (∷ʳ-injective xs ys eq′)
   ∷ʳ-injective []          (_ ∷ _ ∷ _) ()
   ∷ʳ-injective (_ ∷ _ ∷ _) []          ()