proposition: Lemma env_subset_tail : forall E' E, envSubset E' E -> envSubset (tail E') (tail E).
proof: Proof. intros; intros p A D. apply varD_tail. apply H. apply varD_tail_rev; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)