Require Export subst0_defs.
(*#* #caption "axioms for the relation $\\PrZ{}{}$",
- "reflexivity", "compaibility", "$\\beta$-contraction", "$\\upsilon$-swap",
+ "reflexivity", "compatibility", "$\\beta$-contraction", "$\\upsilon$-swap",
"$\\delta$-expansion", "$\\zeta$-contraction", "$\\epsilon$-contraction"
*)
(*#* #cap #cap t, t1, t2 #alpha u in V, u1 in V1, u2 in V2, v1 in W1, v2 in W2, w in T, k in z *)