proposition: Theorem all_binds_binds : forall A x (v : A) (E : gen_env A), (x ∶ v) ⊏ E -> x ∹ v ⋲ E.
proof: Proof. unfold all_binds. intros A x v E Habind. apply (Habind x v). apply binds_single; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv