proposition: Theorem ok_dom_inv : forall A (E : gen_env A), ok E -> List.NoDup (dom E).
proof: Proof. induction E using env_ind; intro Hok. rewrite dom_empty. apply List.NoDup_nil. apply ok_concat_inv in Hok. destruct Hok as [ HokE Hok ] ; destruct Hok as [ Hokx Hdoms ]. destruct Hdoms as [ Hdom1 Hdom2 ]. rewrite dom_concat. rewrite dom_single in *. simpl. apply List.NoDup_cons; auto. apply all_notin_notin in Hdom2. destruct Hdom2. apply notin_dom; auto. Qed.
imports: Utf8 Equalities CoreGenericEnv