proposition: Lemma fresh_string_R_wf {A} s (m : stringmap A) : well_founded (R s m).
proof: Proof. induction (map_wf m) as [m _ IH]. intros n1; constructor; intros n2 [Hn Hs]. specialize (IH _ (delete_subset m (s +:+ pretty (n2 - 1)) Hs) n2). cut (n2 - 1 < n2); [|lia]. clear n1 Hn Hs; revert IH; generalize (n2 - 1). intros n1. induction 1 as [n2 _ IH]; constructor; intros n3 [??]. apply IH; [|lia]; split; [lia|]. by rewrite lookup_delete_ne by (intros ?; simplify_eq/=; lia). Qed.
imports: stdpp(gmap) stdpp(options)