+(*#* #caption "axioms for strict substitution in contexts",
+ "substituted tail item: second operand",
+ "substituted tail item: first operand",
+ "substituted tail item: both operands"
+*)
+(*#* #cap #cap c, c1, c2 #alpha v in W, u in V, u1 in V1, u2 in V2, k in z, r in q *)
+