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