proposition: Lemma simpl_subst_rec : forall N M n p k, p <= n + k -> k <= p -> subst_rec N (lift_rec (S n) M k) p = lift_rec n M k.
proof: Proof. simple induction M; simpl in |- *; intros; auto with coc core arith sets. elim (le_gt_dec k n); intros. rewrite subst_ref_gt; auto with coc core arith sets. red in |- *; red in |- *. apply le_trans with (S (n0 + k)); auto with coc core arith sets. rewrite subst_ref_lt; auto with coc core arith sets. apply le_gt_trans with k; auto with coc core arith sets. rewrite H; auto with coc core arith sets; rewrite H0; auto with coc core arith sets. elim plus_n_Sm with n k; auto with coc core arith sets. rewrite H; auto with coc core arith sets; rewrite H0; auto with coc core arith sets. rewrite H; auto with coc core arith sets; rewrite H0; auto with coc core arith sets. elim plus_n_Sm with n k; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations