proposition: Lemma env_sum_assoc : forall (E1 E2 E3: Env), E1 [+] E2 [+] E3 = E1 [+] (E2 [+] E3).
proof: Proof. induction E1; intros. autorewrite with terms using trivial. destruct E2; destruct E3; autorewrite with terms using trivial. destruct o; destruct o0; simpl; rewrite IHE1; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)