Require Export subst0_defs.
Require Export drop_defs.
-(*#* #caption "current axioms for strict substitution in contexts",
+(*#* #caption "axioms for strict substitution in contexts",
"substituted tail item: second operand",
"substituted tail item: first operand",
"substituted tail item: both operands"