Outline proof for exceptions in Call
Fixed/Proved non exceptional returning calls