include "basics/list.ma". include "ASM/Char.ma". definition String ≝ list Char.