proposition: Lemma env_eq_empty : forall E, emptyEnv E -> E [=] EmptyEnv.
proof: Proof. intros; split. intros w A wA. exfalso; apply (varD_UD_absurd wA). apply H. apply env_subset_empty. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)