Redex sketching.  Don't know how to deal with E-Spawn-Handler yet.