proposition: Theorem all_binds_empty_r : forall A (E : gen_env A), E ⊏ (@empty A) -> E = (@empty A).
proof: Proof. induction E as [ | E x v IHE ] using env_ind; intro Habind; auto. unfold all_binds in Habind. assert (x ∹ v ⋲ (@empty A)) as Hempty by (apply Habind; assert (x ∹ v ⋲ (E & (x ∶ v))) by (apply binds_concat_r; apply binds_single; auto); auto). apply binds_empty in Hempty. inversion Hempty. Qed.
imports: Utf8 Equalities CoreGenericEnv