Require Export subst0_defs.
Require Export csubst0_defs.
-(*#* #caption "axioms for strict substitution in focalized terms",
+(*#* #caption "\\kern-1.2pt axioms for strict substitution in focalized terms",
"substituted term part",
"substituted context part",
"substituted both parts"