proposition: Theorem binds_all_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 Hbind y w Hbind2. apply binds_single_inv in Hbind2. destruct Hbind2; subst; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv