proposition: Lemma env_comp_sum : forall E1 E2 E3, E1 [<->] E2 -> E1 [<->] E3 -> E1 [<->] E2 [+] E3.
proof: Proof. induction E1. intros; apply env_comp_sym; apply env_comp_empty. intros E2 E3 E12 E13. destruct E2. rewrite env_sum_empty_l; trivial. destruct E3. rewrite env_sum_empty_r; trivial. destruct o0; simpl. apply env_comp_cons. apply IHE1; eapply env_comp_tail; eauto. destruct a; try_solve. left; rewrite (E13 0 s0 s); try_solve. apply env_comp_cons. apply IHE1; eapply env_comp_tail; eauto. destruct a; destruct o; try_solve. left; rewrite (E12 0 s s0); try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)