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