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