#reduce "".data

example : "".data = [] := rfl

theorem ex : "".data = [] := rfl