proposition: Lemma env_eq_empty_empty : forall E E', emptyEnv E -> emptyEnv E' -> E [=] E'.
proof: Proof. intros; split; intros p A D. destruct (H p); inversion D; try_solve. destruct (H0 p); inversion D; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)