Finished safety proof for rowan's.  Added let.
safety done, save for prev and lam@1