Signed-off-by: Jim Pryor <profjim@jimpryor.net>
M ~~> N
-We'll mean that you can get from M to N by one or more reduction steps. Hankin uses the symbol <code><big>→</big></code> for one-step contraction, and the symbol <code><big>↠</big></code> for zero-or-more step reduction. Hindley and Seldin use <code><big>⊳</big><sub>1</sub></code> and <code><big>⊳</big></code>.
+We'll mean that you can get from M to N by one or more reduction steps. Hankin uses the symbol <code><big><big>→</big></big></code> for one-step contraction, and the symbol <code><big><big>↠</big></big></code> for zero-or-more step reduction. Hindley and Seldin use <code><big><big><big>⊳</big></big></big><sub>1</sub></code> and <code><big><big><big>⊳</big></big></big></code>.
When M and N are such that there's some P that M reduces to by zero or more steps, and that N also reduces to by zero or more steps, then we say that M and N are **beta-convertible**. We'll write that like this: