proposition: Lemma empty_presubst_neutral_aux : forall Pt i G, (forall x, In x G -> x = None) -> Pt = presubst_aux Pt i G.
proof: Proof. induction Pt. unfold presubst, presubst_aux. intros. destruct (nth_error_In G x) as [[Gx Gx_nth] | Gxn]. rewrite Gx_nth. rewrite (H Gx (nth_some_in G x Gx_nth)); trivial. rewrite Gxn; trivial. auto. intros i G Gempty; simpl. assert (Pt = presubst_aux Pt (S i) (None::G)). apply IHPt; trivial. intros x xIn. destruct xIn. congruence. apply Gempty; trivial. congruence. intros i G Gempty; simpl. assert (Pt1 = presubst_aux Pt1 i G). apply (IHPt1 i G); trivial. assert (Pt2 = presubst_aux Pt2 i G). apply (IHPt2 i); trivial. congruence. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)