proposition: Lemma idSubst_neutral_aux : forall M n, presubst_aux (term M) n (copy n None ++ idSubst M) = term M.
proof: Proof. destruct M as [E Pt A M]. simpl; gen E. induction M; intros E0 n; try_solve. destruct (lt_eq_lt_dec x n) as [[x_lt_n | x_eq_n] | x_gt_n]. rewrite nth_app_left. rewrite nth_copy_in; trivial. autorewrite with datatypes using trivial. rewrite nth_app_right; autorewrite with datatypes. rewrite x_eq_n. rewrite (Nat.sub_diag n); simpl. destruct (isVarDecl_dec E0 0) as [[B EB] | En]; trivial. lia. rewrite nth_beyond; trivial. rewrite length_app. autorewrite with datatypes. destruct (isVarDecl_dec E0 0) as [[B EB] | En]; simpl; lia. set (hint := IHM E0 (S n)). set (Pt2 := Pt) in |- * at 1. rewrite <- hint. unfold Pt2; clear hint. destruct (isVarDecl_dec E0 0) as [[C EC] | En]; trivial. set (PtL' := PtL) in |- * at 1. set (PtR' := PtR) in |- * at 1. rewrite <- (IHM1 E0 n). rewrite <- (IHM2 E0 n). destruct (isVarDecl_dec E n) as [[C EC] | en]; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)