From f07f75192b4359b41d5b13067cafa33151f2ea25 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 4 Sep 2024 16:45:57 +1000
Subject: [PATCH] imports

---
 src/Init/Data/Bool.lean        | 2 +-
 src/Init/Data/List/Lemmas.lean | 3 +--
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index ce29d5d6402e..c83d631afae6 100644
--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: F. G. Dorais
 -/
 prelude
-import Init.BinderPredicates
+import Init.NotationExtra
 
 /-- Boolean exclusive or -/
 abbrev xor : Bool → Bool → Bool := bne
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 7c28ca3a8e1d..9452041e1d3f 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -8,9 +8,8 @@ import Init.Data.Bool
 import Init.Data.Option.Lemmas
 import Init.Data.List.BasicAux
 import Init.Data.List.Control
-import Init.PropLemmas
 import Init.Control.Lawful.Basic
-import Init.Hints
+import Init.BinderPredicates
 
 /-! # Theorems about `List` operations.