Removed succ₁≡succ.
Fixed typos.
Added fixed-points definitions.
s/*-ir/*-in.
Fixed typos.
s/*-pre-fixed/*-in.