(* literal, substitutions.
* Some [] -> user has given an empty explicit substitution list
* None -> user has given no explicit substitution list *)
(* literal, substitutions.
* Some [] -> user has given an empty explicit substitution list
* None -> user has given no explicit substitution list *)