use :: instead of : for declarations, since : appears reserved in redex
fix typo-bug
preservation failure, showing the need for path dual
add dual rule
intermediate preservation failure caused by dual rule