proposition: Lemma tail_distr_sum : forall E1 E2, tail (E1 [+] E2) = tail E1 [+] tail E2.
proof: Proof. intros. destruct E1; destruct E2; try destruct E2; try destruct o0; try_solve. rewrite env_sum_empty_r; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)