proposition: Lemma ok_concat_map: forall E F (f : A -> A), ok (E & F) -> ok (E & map f F).
proof: Proof. Proof using. induction F 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)