proposition: Lemma distr_subst_rec : forall M N (P : term) n p, subst_rec P (subst_rec N M p) (p + n) = subst_rec (subst_rec P N n) (subst_rec P M (S (p + n))) p.
proof: Proof. simple induction M; auto with coc core arith sets; intros. unfold subst_rec at 2 in |- *. elim (lt_eq_lt_dec p n); [ intro Hlt_eq | intro Hlt ]. elim Hlt_eq; clear Hlt_eq. case n; [ intro Hlt | intros n1 Heq1 ]. inversion_clear Hlt. unfold pred, subst_rec at 1 in |- *. elim (lt_eq_lt_dec (p + n0) n1); [ intro Hlt_eq | intro Hlt ]. elim Hlt_eq; clear Hlt_eq. case n1; [ intro Hlt | intros n2 Heq2 ]. inversion_clear Hlt. rewrite subst_ref_gt; auto with coc core arith sets. rewrite subst_ref_gt; auto with coc core arith sets. apply gt_le_trans with (p + n0); auto with coc core arith sets. simple induction 1. rewrite subst_ref_eq; auto with coc core arith sets. rewrite simpl_subst; auto with coc core arith sets. rewrite subst_ref_lt; auto with coc core arith sets. rewrite subst_ref_gt; auto with coc core arith sets. simple induction 1. rewrite subst_ref_lt; auto with coc core arith sets. rewrite subst_ref_eq. unfold lift in |- *. rewrite commut_lift_subst_rec; auto with coc core arith sets. do 3 (rewrite subst_ref_lt; auto with coc core arith sets). simpl in |- *; replace (S (p + n)) with (S p + n); auto with coc core arith sets. rewrite H; auto with coc core arith sets; rewrite H0; auto with coc core arith sets. simpl in |- *; rewrite H; rewrite H0; auto with coc core arith sets. simpl in |- *; replace (S (p + n)) with (S p + n); auto with coc core arith sets. rewrite H; rewrite H0; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations