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