diff --git a/blueprint/src/sections/sec10/10-2_spacetime.tex b/blueprint/src/sections/sec10/10-2_spacetime.tex
index bcde896..41babb4 100644
--- a/blueprint/src/sections/sec10/10-2_spacetime.tex
+++ b/blueprint/src/sections/sec10/10-2_spacetime.tex
@@ -308,7 +308,7 @@ \section{Spacetime}\label{sctn:spacetime}
 
 \begin{lemma}[Chronological Precedence Implies Causal Precedence]
     \label{lmm:chronological-implies-causal}
-    \lean{Physicslib4.Spacetime.isCausal_of_isTimelike, Physicslib4.Spacetime.isCausalTrip_of_isTrip, Physicslib4.Spacetime.causallyPrecedes_of_chronologicallyPrecedes, Physicslib4.Spacetime.chronologicalFuture_subset_causalFuture, Physicslib4.Spacetime.chronologicalPast_subset_causalPast}
+    \lean{Physicslib4.Spacetime.isCausal_of_isTimelike, Physicslib4.Spacetime.causallyPrecedes_of_chronologicallyPrecedes, Physicslib4.Spacetime.chronologicalFuture_subset_causalFuture, Physicslib4.Spacetime.chronologicalPast_subset_causalPast}
     \leanfile{Physicslib4/Spacetime/Causality.lean}
     \leanok
     \uses{def:trip, def:causal-trip, def:chronological-future-and-chronological-past, def:causal-future-and-causal-past}