proposition: Lemma binds_functional : forall x v1 v2 E, binds x v1 E -> binds x v2 E -> v1 = v2.
proof: Proof. Proof using. introv H1 H2. unfolds binds. induction E as [|E' x' v'] using env_ind. rewrite get_empty in H1. false. rewrite get_push in H1,H2. case_if~. inverts H1. inverts~ H2. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)