start updating proofs for addition of mlstrings

not all done yet