proposition: Lemma env_sum_sub : forall E1 E2 E3, (forall p, E2 |= p :! \/ E3 |= p :!) -> E1 [+] E2 [-] E3 = E1 [-] E3 [+] E2.
proof: Proof. induction E1; intros F G H. rewrite env_sub_disjoint; trivial. rewrite env_sum_empty_l; trivial. destruct F; destruct G; destruct a; repeat rewrite env_sum_empty_r; repeat rewrite env_sub_empty; simpl; trivial. destruct o; destruct o0; try_solve; try solve [ rewrite (IHE1 F G); [trivial | intro p; exact (H (S p))] | destruct (H 0); destruct H0; try_solve ]. destruct o; destruct o0; try solve [ simpl; rewrite (IHE1 F G); [trivial | intro p; exact (H (S p))] | destruct (H 0); destruct H0; try_solve ]. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)