proposition: Lemma img_concat : forall E F, img (E & F) = List.app (img F) (img E).
proof: Proof. intros E F; generalize E; induction F as [ | (x, v) F IHF ]; intros; simpl in *; auto. rewrite IHF. reflexivity. Qed.
imports: Utf8 Equalities