proposition: Theorem binds_single : forall A x y (v w : A), x = y -> v = w -> x ∹ v ⋲ (y ∶ w).
proof: Proof. intros A x y v w Heq1 Heq2. rewrite Heq1, Heq2. unfold binds. rewrite get_single_eq; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv