fix: add grind annotations and a lemma#435

Shreyas4991 wants to merge 4 commits intoleanprover:mainleanprover/cslib:mainfrom

Shreyas4991:freem-improvementsShreyas4991/cslib:freem-improvementsCopy head branch name to clipboard