proposition: Lemma natmap_cons_canon_wf {A} (o : option A) (l : natmap_raw A) : natmap_wf l → natmap_wf (natmap_cons_canon o l).
proof: Proof. unfold natmap_wf, last. destruct o, l; simpl; eauto. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)