proposition: Lemma lift_tail : forall E n k, liftedEnv n (tail E) k [=] tail (liftedEnv n E (S k)).
proof: Proof. induction E; intros. unfold liftedEnv, finalSeg; destruct k; simpl; rewrite <- 1app_nil_end. apply env_eq_empty_empty. apply emptyEnv_copyNone. apply tail_emptyEnv. apply emptyEnv_copyNone. apply env_eq_empty_empty. apply emptyEnv_copyNone. apply tail_emptyEnv. apply emptyEnv_copyNone. unfold liftedEnv; simpl. change (finalSeg (a::E) (S k)) with (finalSeg E k). apply env_eq_refl. Qed.
imports: CoLoR(RelExtras ListExtras TermsLifting LogicUtil OptUtil) Coq(Arith Setoid Morphisms Lia)