proposition: Lemma env_sum_ry : forall E1 E2 x A, E2 |= x := A -> E1 [+] E2 |= x := A.
proof: Proof. induction E1; destruct E2; intros x A E_comp; try solve [unfold VarD; destruct x; simpl; intros; discr]. auto. unfold VarD; simpl. destruct o; destruct x; simpl; intros; solve [trivial | discr | apply IHE1; trivial]. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)