get translation proofs through
fix autosubst stuff
extend step relation to let you step into pairs
redefine translation in a new way
prove simulation