proposition: Theorem binds_eq_inv : forall A x (v w : A) (E : gen_env A), x ∹ v ⋲ E -> x ∹ w ⋲ E -> v = w.
proof: Proof. intros A x v w E Hbind1 Hbind2. inversion Hbind1 as [ Hget1 ]. inversion Hbind2 as [ Hget2 ]. rewrite Hget1 in Hget2. inversion Hget2; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv