diff --git a/theories/Core/Completeness/TermStructureCases.v b/theories/Core/Completeness/TermStructureCases.v
index bfd8c44d..1151b42c 100644
--- a/theories/Core/Completeness/TermStructureCases.v
+++ b/theories/Core/Completeness/TermStructureCases.v
@@ -1,5 +1,5 @@
 From Coq Require Import Morphisms_Relations RelationClasses.
-From Mcltt Require Import Base LibTactics LogicalRelation System.
+From Mcltt Require Import Base LibTactics Completeness.LogicalRelation System.
 Import Domain_Notations.
 
 Lemma rel_exp_sub_cong : forall {Δ M M' A σ σ' Γ},
diff --git a/theories/Core/Completeness/UniverseCases.v b/theories/Core/Completeness/UniverseCases.v
index 6b55077c..5e7bab52 100644
--- a/theories/Core/Completeness/UniverseCases.v
+++ b/theories/Core/Completeness/UniverseCases.v
@@ -1,5 +1,5 @@
 From Coq Require Import Morphisms_Relations.
-From Mcltt Require Import Base LibTactics LogicalRelation.
+From Mcltt Require Import Base LibTactics Completeness.LogicalRelation.
 Import Domain_Notations.
 
 Lemma valid_typ : forall {i Γ},
diff --git a/theories/Core/Completeness/VariableCases.v b/theories/Core/Completeness/VariableCases.v
index 3d3d04e8..09774287 100644
--- a/theories/Core/Completeness/VariableCases.v
+++ b/theories/Core/Completeness/VariableCases.v
@@ -1,5 +1,5 @@
 From Coq Require Import Morphisms_Relations Relations.
-From Mcltt Require Import Base LibTactics LogicalRelation System.
+From Mcltt Require Import Base LibTactics Completeness.LogicalRelation System.
 Import Domain_Notations.
 
 Lemma valid_lookup : forall {Γ x A env_rel}