proposition: Lemma get_single : forall k x v, get k (x ~ v) = If k = x then Some v else None.
proof: Proof. Proof using. intros. rew_env_defs. unfold get_impl. auto. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)