proposition: Lemma pre_from_elements_OK : forall A l dom (m : t A dom), OK (fold_left (fun acc xv => Dom.add (fst xv) acc) l (domain m)) (fold_left (fun acc xv => S.add (fst xv) (snd xv) acc) l (proj1_sig m)).
proof: Proof. intros A l. induction l as [| [x v] l]; intros dom m; simpl; unfold domain. + apply (proj2_sig m). + change (Dom.add x dom) with (domain (add x v m)). change (S.add x v (proj1_sig m)) with (proj1_sig (add x v m)). apply IHl. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface