definition sh_N: sh ≝ mk_sh S ….
// defined.