proposition: Lemma env_sub_Empty : forall E1 E2, emptyEnv E2 -> E1 [-] E2 = E1.
proof: Proof. induction E1; trivial. intros E2 E2_empty; simpl. destruct a; destruct E2; try destruct o; trivial; try solve [ rewrite IHE1; [trivial | apply emptyEnv_tail; trivial] | eapply emptyEnv_absurd; eauto ]. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)