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