proposition: Lemma ok_remove : forall F E G, ok (E & F & G) -> ok (E & G).
proof: Proof. Proof using. induction G using env_ind; rew_env_concat; introv Ok. lets*: ok_concat_inv Ok. lets*: ok_push_inv Ok. Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)