proposition: Lemma natmap_wf_lookup {A} (l : natmap_raw A) : natmap_wf l → l ≠ [] → ∃ i x, mjoin (l !! i) = Some x.
proof: Proof. intros Hwf Hl. induction l as [|[x|] l IH]; simpl; [done| |]. { exists 0. simpl. eauto. } destruct IH as (i&x&?); eauto using natmap_wf_inv; [|by exists (S i), x]. intros ->. by destruct Hwf. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)