Proof using: do not clear letins (unless they use a cleared var)