proposition: Lemma get_concat : forall k E F, get k (E & F) = match get k F with | None => get k E | Some v => Some v end.
proof: Proof. Proof using. intros. rew_env_defs. induction F as [|(x,v)]; rew_list. auto. simpl. case_if~. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)