proposition: Theorem eq_update : forall A (E F G : gen_env A), E ≍ F -> (E ::= G) ≍ (F ::= G).
proof: Proof. intros A E F G Heq. unfold eq in *. destruct Heq. split; apply all_binds_update; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv