proposition: Theorem eq_get_inv : forall A (E F : gen_env A), (forall x, get x E = get x F) -> E ≍ F.
proof: Proof. intros A E F Hyp. unfold eq, all_binds, binds. split; intros x v Hbind. rewrite <- Hbind; auto. rewrite Hyp; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv