proposition: Lemma env_sum_ly : forall E1 E2 x A, env_comp_on E1 E2 x -> E1 |= x := A -> E1 [+] E2 |= x := A.
proof: Proof. intros; destruct (isVarDecl_dec E2 x) as [[B E2x] | E2xn]. unfold VarD; rewrite (env_sum_ry E1 E2x). assert (A = B); [apply H; trivial | congruence]. apply env_sum_ly_rn; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)