proposition: Lemma binds_middle_eq : forall x E1 E2 v, x # E2 -> binds x v (E1 & x ~ v & E2).
proof: Proof. Proof using. introv F. applys~ binds_concat_left. applys binds_tail. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)