proposition: Lemma env_subset_lsum : forall El Er E, envSubset El E -> envSubset Er E -> envSubset (El [+] Er) E.
proof: Proof. intros; intros p A D. destruct (env_sum_varDecl El Er D) as [[Elp _] | Erp]. apply H; trivial. apply H0; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)