proposition: Theorem belongs_all_binds : forall A x (F : gen_env A), x ∈ F -> exists v, (x ∶ v) ⊏ F.
proof: Proof. intros A x F Hin. unfold all_binds. apply belongs_binds in Hin. destruct Hin as [ v Hbind ]. exists v. intros y w Hbind2. apply binds_single_inv in Hbind2. destruct Hbind2; subst; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv