proposition: Lemma presubst_var_beyond G i x : x >= length G -> presubst_aux (%x) i G = %x.
proof: Proof. intro x_G. rewrite subst_lift_subst. change (%x) at 1 with (prelift_aux x (%0) 0). change (lift_subst G i) with (copy 0 None ++ lift_subst G i). rewrite presubst_lift_beyond; trivial. rewrite length_lift_subst; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)