proposition: Theorem all_binds_map : forall A B (f : A -> B) (E F : gen_env A), E ⊏ F -> map f E ⊏ map f F.
proof: Proof. intros A B f E F Habind. unfold all_binds in *. intros x v Hbind. apply binds_map_inv in Hbind. destruct Hbind as [ w [ Hbind Heq ] ]. apply Habind in Hbind. subst. apply binds_map. auto. Qed.
imports: Utf8 Equalities CoreGenericEnv