proposition: Lemma list_to_natmap_spec {A} (l : list (option A)) i : list_to_natmap l !! i = mjoin (l !! i).
proof: Proof. unfold lookup at 1, natmap_lookup, list_to_natmap; simpl. rewrite <-(reverse_involutive l) at 2. revert i. induction (reverse l) as [|[x|] l' IH]; intros i; simpl; auto. rewrite reverse_cons, IH. clear IH. revert i. induction (reverse l'); intros [|?]; simpl; auto. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)