The Lemmas tutorial
states and proves a "distributive lemma" of the
function. However, the lemmas statement is not type correct, because
but the lemmas passes
The tutorial also refers to "How Dafny Works". I didn't find anything useful by googling that phrase. What is this referring to?