proposition: Lemma env_sum_disjoint : forall E1 E2, (copy (length E1) None ++ E2) [+] E1 = E1 ++ E2.
proof: Proof. induction E1; simpl; intros. rewrite env_sum_empty_r; trivial. destruct a; rewrite IHE1; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)