S x = y (= (S x) y) apply > infix operators
\forall x.x=x (\forall x.(= x x)) infix operators > binders
\lambda x.x \to x \lambda. (x \to x) \to > \lambda
S x = y (= (S x) y) apply > infix operators
\forall x.x=x (\forall x.(= x x)) infix operators > binders
\lambda x.x \to x \lambda. (x \to x) \to > \lambda