remove redundant word
extend target calculus step relation as in the paper
include autosubst into translation module
begin trying to prove simulation
add missing step relations
fix incorrect translation
add some notation
add translation correctness proofs