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