proposition: Lemma env_subset_sum : forall El El' Er Er', El' [<->] Er' -> envSubset El El' -> envSubset Er Er' -> 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. exact (H p). apply H0; trivial. apply env_sum_ry. apply H1; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)