proposition: Lemma env_eq_subset_sum_l : forall E E', envSubset E' E -> E [=] E' [+] E.
proof: Proof. intros; split. apply env_subset_sum_r; apply env_subset_refl. intros w A D. destruct (env_sum_varDecl E' E D) as [[E'w _] | Ew]; trivial. apply H; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)