doc: Clarify the precondition of the conf'-lemma

Author: ibbem

src/Translation/Lang/FST-to-VariantList.agda

@@ -186,9 +186,9 @@ and then evaluating the configuration at the index of `c` (which must be `c`),
 is the same as evaluating `c` directly.
 
 The lemma talks about `conf'` instead of `conf` and inlines `fnoc` to avoid extracting the `name` all the time.
-Note that if a feature `f` is not in the list of features of the `SPL` expression,
-we just set the configuration in `configs` to `false`.
-Hence, it can be different to a given configuration `c`.
+Note that `f ∈ fs` is a necessary requirement
+because configurations generated by `configs` are always set to `false` if `f ∉ fs`
+whereas the given configuration `c` can have arbitrary values for any input.
 
 The proof does an induction on the list of features
 and makes a case analysis,