proposition: Theorem all_binds_single_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 Habind1 Habind2. apply all_binds_binds in Habind1. apply all_binds_binds in Habind2. apply binds_eq_inv with x E; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv