Split forward simulation assumptions.
Fix backward refinement.
Fix rest of proofs.
Merge branch 'split-assumptions'