proposition: Theorem binds_single_inv : forall A x y (v w: A), x ∹ v ⋲ (y ∶ w) -> x = y ∧ v = w.
proof: Proof. intros A x y v w Hbind. inversion Hbind as [ Hget ]. destruct (eq_var_dec x y) as [ Heq | Hneq ]. rewrite Heq in *; clear x Heq. rewrite get_single_eq in Hget; auto. inversion Hget; auto. apply get_single_eq_inv in Hget. destruct Hget; contradiction. Qed.
imports: Utf8 Equalities CoreGenericEnv