[squash] remove half-thought

docs/arch-split.md

@@ -646,9 +646,7 @@ interpretation Foo_AI_2?: Foo_AI_2
 FIXME: strictly speaking, there is no requirement that `Foo_AI_2` includes
 `Foo_AI_1`, but in practice we always do so (I guess because we want everything
 that got proved to be instantly available in case we need it in the proof
-chain). This would mean that the same fact gets exported multiple times? Are
-there downsides to this? This also affects whether
-
+chain). This would mean that the same fact gets exported multiple times?
 
 ## Qualifying non-locale-compatible commands