[squash] address FIXMEs after PR comments/discussion

docs/arch-split.md

@@ -296,7 +296,6 @@ multiple facts).
 
 This disparity will only get worse as the Arch context grows bigger, and
 might indicate the need for some alternative functionality.
-(FIXME: check if this is true)
 
 
 ### Dealing with name clashes
@@ -643,10 +642,12 @@ interpretation Foo_AI_2?: Foo_AI_2
 (* now we get access to GD in the global context *)
 ```
 
-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?
+While strictly speaking, there is no requirement that `Foo_AI_2` includes
+`Foo_AI_1`, in practice we always do so, since we want everything that got
+proved to be instantly available in case it's needed in the proof chain. This
+generates limited duplication: a fact from `Foo_AI_1` will be duplicated in
+`Foo_AI_2`, but not in `Foo_AI_3+`.
+
 
 ## Qualifying non-locale-compatible commands