include "Char.ma".
include "List.ma".

ndefinition String ≝ List Char.