proposition: Theorem all_binds_map_inv : forall A B (f : A -> B) (E F : gen_env A), Image.injective A B f -> map f E ⊏ map f F -> E ⊏ F.
proof: Proof. intros A B f E F Hinj Habind. unfold all_binds in *. intros x v Hbind. assert (x ∹ (f v) ⋲ map f E) as Hbind2 by (apply binds_map; auto). apply Habind in Hbind2. apply binds_map_inv in Hbind2. destruct Hbind2 as [ w [ Hbind2 Heq ] ]. unfold Image.injective in *. apply Hinj in Heq. rewrite Heq; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv