proposition: Lemma list_to_natmap_wf {A} (l : list (option A)) : natmap_wf (reverse (strip_Nones (reverse l))).
proof: Proof. unfold natmap_wf. rewrite last_reverse. induction (reverse l) as [|[]]; simpl; eauto. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)