proposition: Lemma presubst_singleton_conv_sim_aux : forall M M' T T' Q R R' i, (forall j, j <= i -> envSub Q j j) -> conv_term M M' Q -> (lift T i) ~(Q) (lift T' i) -> conv_term R R' Q -> presubst_aux M i (copy i None ++ {x/T}) = R -> presubst_aux M' i (copy i None ++ {x/T'}) = R'.
proof: Proof. induction M; unfold presubst; simpl; intros; inversion H0; rewrite <- H3 in H2. destruct (lt_eq_lt_dec i x) as [[i_x | i_x] | i_x]. rewrite nth_beyond in H2. inversion H2. simpl; rewrite nth_beyond. cut (y = y0); auto. apply envSub_Lok with Q x; trivial. autorewrite with datatypes using simpl. destruct (le_gt_dec y i). absurd (x = y). lia. apply envSub_Rok with Q y; trivial. apply H; trivial. lia. autorewrite with datatypes using simpl; try lia. rewrite nth_app_right in H2; autorewrite with datatypes using try lia. replace (x - length (copy i (None (A:=Term)))) with 0 in H2. simpl in H2. destruct H1. assert (x = y). apply envSub_Lok with Q x; trivial. apply H; lia. rewrite <- H9; simpl. rewrite nth_app_right; autorewrite with datatypes. replace (x - i) with 0; simpl. apply conv_term_unique with (term (lift T i)) Q; trivial. lia. lia. autorewrite with datatypes using lia. rewrite nth_app_left in H2; autorewrite with datatypes using trivial. rewrite nth_copy_in in H2; trivial. assert (x = y). apply envSub_Lok with Q x; trivial. apply H; lia. rewrite <- H8; simpl. rewrite nth_app_left; autorewrite with datatypes using trivial. inversion H2. cut (x = y0); auto. rewrite <- H8 in H5. apply envSub_Lok with Q x; trivial. inversion H2; trivial. inversion H2. change (None :: copy i None ++ {x/T'}) with (copy (Datatypes.S i) None ++ {x/T'}). assert (presubst_aux R0 (Datatypes.S i) (copy (Datatypes.S i) None ++ {x/T'}) = R1). apply (@IHM R0 T T' (envSubst_lift1 Q) L0 R1 (Datatypes.S i)); auto. intros j j_i; destruct j; destruct Q; simpl; trivial. apply H; lia. rewrite <- (lift_fold_1out T). rewrite <- (lift_fold_1out T'). apply terms_conv_conv_lift; trivial. rewrite H11; trivial. try_solve. inversion H2. simpl. rewrite (IHM1 RL T T' Q LL0 RL0); auto. rewrite (IHM2 RR T T' Q LR0 RR0); auto. rewrite H11; trivial. rewrite H10; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubst) Coq(Arith Lia)