proposition: Lemma varD_tail : forall E A i, E |= S i := A -> tail E |= i := A.
proof: Proof. intros; destruct E; trivial. inversion H. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)