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