a lemma function is introduced with 'let lemma f' or 'let rec lemma f'
it is a ghost function
it must have return type unit and read-only effects
it introduces a goal (its WP), followed by an axiom
  forall args/reads, precondition => postcondition