proposition: Lemma singleton_presubst : forall M P G i j, isSingletonSubst P G -> presubst_aux (term M) j (copy i None ++ {x/P}) = presubst_aux (term M) j (copy i None ++ G).
proof: Proof. destruct M as [E Pt T M]; induction M; intros; unfold presubst; simpl in * . destruct (lt_eq_lt_dec x i) as [[x_i | x_i] | x_i]. rewrite !nth_app_left; autorewrite with datatypes; solve [lia | trivial]. rewrite x_i. rewrite !nth_app_right; autorewrite with datatypes; try lia. replace (i - i) with 0; [simpl | lia]. destruct G. inversion H; inversion H0. destruct o; inversion H; inversion H0. rewrite <- H3; trivial. rewrite !nth_app_right; autorewrite with datatypes; try lia. assert (x - i > 0); [lia | destruct (x - i)]. lia. destruct G. inversion H; inversion H1. destruct o; simpl. replace (nth_error (A:=option Term) nil n) with (None (A:=option Term)). inversion H. destruct (H2 n); simpl in H3; rewrite H3; trivial. destruct n; trivial. inversion H; inversion H1. trivial. rewrite !app_comm_cons. change ((None (A:=Term)) :: copy i None) with (copy (S i) (None (A:=Term))). rewrite (IHM P G (S i) (S j)); trivial. rewrite (IHM1 P G i j); trivial. rewrite (IHM2 P G i j); trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsConv ListUtil ListExtras LogicUtil) Coq(Arith Lia)