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.