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