Fixed mistake in "Putting it all together" page in docs#2247

parno merged 2 commits intoverus-lang:mainverus-lang/verus:mainfrom

jsenn:user/jsenn/doc-fixjsenn/verus:user/jsenn/doc-fixCopy head branch name to clipboard