proposition: Lemma empty_middle_inv : forall E F x v, empty = E & x ~ v & F -> False.
proof: Proof. Proof using. introv H. rew_env_defs. forwards* [_ ?]: nil_eq_app_inv H. false. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)