proposition: Lemma env_sum_ly_rn : forall E1 E2 x A, E1 |= x := A -> E2 |= x :! -> E1 [+] E2 |= x := A.
proof: Proof. induction E1; destruct E2 as [|a' E2]; trivial. inversion 1; destruct x; discr. inversion 1; inversion 1; destruct a'; destruct x; unfold VarD; simpl in *; solve [trivial | discr | apply IHE1; trivial]. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)