proposition: Lemma concat_assoc_map_push : forall f E F x v, E & (map f (F & x ~ v)) = (E & map f F) & x ~ (f v).
proof: Proof. Proof using. intros. rewrite map_concat. rewrite map_single. rewrite~ concat_assoc. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)