proposition: Lemma ok_push_inv : forall E x v, ok (E & x ~ v) -> ok E /\ x # E.
proof: Proof. Proof using. intros. inverts H as H1 H2. false (empty_push_inv H1). destructs 3 (eq_push_inv H). subst~. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)