proposition: Lemma env_eq_empty_subset : forall E E', E [=] EmptyEnv -> envSubset E E'.
proof: Proof. intros. intros w A wA. set (x := (proj1 H) w A wA). destruct w; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)