proposition: Lemma commut_lift_subst_rec : forall M N n p k, k <= p -> lift_rec n (subst_rec N M p) k = subst_rec N (lift_rec n M k) (n + p).
proof: Proof. simple induction M; intros; auto with coc core arith sets. unfold subst_rec at 1, lift_rec at 2 in |- *. elim (lt_eq_lt_dec p n); [ intro Hlt_eq; elim (le_gt_dec k n); [ intro Hle | intro Hgt ] | intro Hlt; elim (le_gt_dec k n); [ intro Hle | intro Hgt ] ]. elim Hlt_eq; clear Hlt_eq. case n; [ intro Hlt | intros ]. inversion_clear Hlt. unfold pred in |- *. rewrite lift_ref_ge; auto with coc core arith sets. rewrite subst_ref_gt; auto with coc core arith sets. elim plus_n_Sm with n0 n1. auto with coc core arith sets. apply le_trans with p; auto with coc core arith sets. simple induction 1. rewrite subst_ref_eq. unfold lift in |- *. rewrite simpl_lift_rec; auto with coc core arith sets. absurd (k <= n); auto with coc core arith sets. apply le_trans with p; auto with coc core arith sets. elim Hlt_eq; auto with coc core arith sets. simple induction 1; auto with coc core arith sets. rewrite lift_ref_ge; auto with coc core arith sets. rewrite subst_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. apply le_gt_trans with p; auto with coc core arith sets. simpl in |- *. rewrite plus_n_Sm. rewrite H; auto with coc core arith sets; rewrite H0; auto with coc core arith sets. simpl in |- *; rewrite H; auto with coc core arith sets; rewrite H0; auto with coc core arith sets. simpl in |- *; rewrite plus_n_Sm. rewrite H; auto with coc core arith sets; rewrite H0; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations