proposition: Lemma lower_tail : forall E n, loweredEnv (tail E) n = tail (loweredEnv E (S n)).
proof: Proof. induction E; intros. destruct n; trivial. unfold loweredEnv; simpl. change (finalSeg (a::E) (S (S n))) with (finalSeg E (S n)); trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)