proposition: Theorem eq_get : forall A (E F : gen_env A), E ≍ F -> forall x, get x E = get x F.
proof: Proof. intros A E F Heq x. unfold eq in Heq. destruct Heq as [ Habind1 Habind2 ]. unfold all_binds in *. unfold binds in *. elim get_dec with A x E; elim get_dec with A x F; intros Hyp1 Hyp2. destruct Hyp1 as [ v Hget1 ]; destruct Hyp2 as [ w Hget2 ]. rewrite Hget1, Hget2. apply Habind1 in Hget2. rewrite Hget1 in Hget2; auto. destruct Hyp2 as [ v Hget2 ]. apply Habind1 in Hget2. rewrite Hyp1 in Hget2. inversion Hget2. destruct Hyp1 as [ v Hget1 ]. apply Habind2 in Hget1. rewrite Hyp2 in Hget1. inversion Hget1. rewrite Hyp1, Hyp2; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv