proposition: Lemma distr_lift_subst_rec : forall M N n p k, lift_rec n (subst_rec N M p) (p + k) = subst_rec (lift_rec n N k) (lift_rec n M (S (p + k))) p.
proof: Proof. simple induction M; intros; auto with coc core arith sets. unfold subst_rec at 1 in |- *. elim (lt_eq_lt_dec p n); [ intro a | intro b ]. elim a; clear a. case n; [ intro a | intros n1 b ]. inversion_clear a. unfold pred, lift_rec at 1 in |- *. elim (le_gt_dec (p + k) n1); intro. rewrite lift_ref_ge; auto with coc core arith sets. elim plus_n_Sm with n0 n1. rewrite subst_ref_gt; auto with coc core arith sets. red in |- *; red in |- *; apply le_n_S. apply le_trans with (n0 + (p + k)); auto with coc core arith sets. apply le_trans with (p + k); auto with coc core arith sets. rewrite lift_ref_lt; auto with coc core arith sets. rewrite subst_ref_gt; auto with coc core arith sets. simple induction 1. unfold lift in |- *. rewrite <- permute_lift_rec; auto with coc core arith sets. rewrite lift_ref_lt; auto with coc core arith sets. rewrite subst_ref_eq; auto with coc core arith sets. rewrite lift_ref_lt; auto with coc core arith sets. rewrite lift_ref_lt; auto with coc core arith sets. rewrite subst_ref_lt; auto with coc core arith sets. simpl in |- *; replace (S (p + k)) with (S p + k); auto with coc core arith sets. rewrite H; 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 + k)) with (S p + k); auto with coc core arith sets. rewrite H; rewrite H0; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations