Unify notation and property/lemma names between Coq and F*
-
Certain properties have different names in the Coq/F* proofs (e.g.,
is_tall
vshas_height
), and the name of certain lemmas. This situation is somewhat documented in the Coq code commentary, but it would be best to unify them. -
Also, we could also pack the [incremental_spec] property in F* as well, in order to make more evident the similarity between pre and post-conditions.
-
The name of higher-level lemmas 'e.g. the incremmentality property, connecting get/insert get/add, should also be renamed.