proposition: Lemma env_sum_remove_double : forall E1 E2, E1 [+] E2 [+] E1 = E2 [+] E1.
proof: Proof. induction E1; intros. destruct E2; trivial. destruct E2; simpl. destruct a; rewrite env_sum_double; trivial. destruct o; destruct a; rewrite <- IHE1; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)