proposition: Lemma ok_middle_inv : forall E F x v, ok (E & x ~ v & F) -> x # E /\ x # F.
proof: Proof. Proof using. induction F using env_ind; introv; rew_env_concat; intros Ok; destruct (ok_push_inv Ok). split~. forwards~ [? ?]: IHF H. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)