touch up compiler proofs for strings

although cheat the case about correct compilation of strings, and
haven't added the new clause to the data refinement relation either.