abstract proofs over checkInsert

All proofs about expressions containing checkInsert share a common
pattern. There are three cases:
 1) Inserting a key-value-pair that is already present in the map.
 2) Inserting a new key into the map.
 3) Failure to insert a conflicting key-value pair in the map.

The checkInsertProof record enables to write three different cases
reducing the usage of "with" (and thus line length) in
lemma-checkInsert-restrict and lemma-lookupM-assoc.

0 files changed, 0 insertions, 0 deletions