update a few proofs in free_varsScript.sml