proposition: Lemma env_eq_tail : forall E1 E2, E1 [=] E2 -> tail E1 [=] tail E2.
proof: Proof. intros. split; destruct H; apply env_subset_tail; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)