proposition: Lemma ok_map : forall E (f : A -> B), ok E -> ok (map f E).
proof: Proof. Proof using. induction E using env_ind; introv; autorewrite with rew_env_map; rew_env_concat; intros Ok. auto. destruct* (ok_push_inv Ok). Qed.
imports: TLC(LibTactics LibOption LibList LibProd LibLogic LibReflect)