proposition: Lemma emptyEnv_cons : forall E, emptyEnv E -> emptyEnv (None :: E).
proof: Proof. intros. intro p; destruct p. right; try_solve. apply (H p). Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)