proposition: Lemma get_push : forall k x v E, get k (E & x ~ v) = If k = x then Some v else get k E.
proof: Proof. Proof using. intros. rewrite get_concat. rewrite get_single. case_if~. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)