proposition: Lemma env_comp_sum_comm : forall E1 E2, E1 [<->] E2 -> E1 [+] E2 = E2 [+] E1.
proof: Proof. induction E1. destruct E2; try_solve. destruct E2. destruct E1; try_solve. intro E12c. set (IH := IHE1 E2 (env_comp_tail E12c)). destruct a; destruct o; simpl; try rewrite IH; trivial. rewrite (E12c 0 s s0); unfold VarD; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)