proposition: Lemma env_subset_empty : forall E, envSubset EmptyEnv E.
proof: Proof. intros; intros p A D. inversion D; destruct p; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)