Date: Mon, 13 Mar 89 11:39:28 PDT The rule C,a<b |- s < t (RL) -------------------------- C |- (rec a s) < (rec b t) appears in \bibitem[Car86]{amber} L.~Cardelli. \newblock Amber. \newblock In {\em Combinators and Functional Programming Languages, LNCS 242}, pages 21--47, 1986.