Drop `DiagNone` precondition of `lookup_merge` rule of `FinMap` interface.

This fixes issue #94 (closed)

• Drop DiagNone class.
• Add merge_proper instance.
• Simplify lemmas about merge by dropping the DiagNone precondition.
• Generalize lemmas partial_alter_merge, partial_alter_merge_l, and partial_alter_merge_r.
• Drop unused merge_assoc' instance, which seems unused, and seems pointless to generalize.

I don't really have a good overview over what happens here, but from a superficial glance, this LGTM -- and I agree with #94 (closed). So, modulo the one nit, feel free to land.

added 1 commit

• 3e4dd120 - Comment about `diag_None`.

Compare with previous version

resolved all threads

merged

mentioned in commit 34e363f0