proposition: Lemma permute_lift_rec : forall M n k p i, i <= k -> lift_rec p (lift_rec n M k) i = lift_rec n (lift_rec p M i) (p + k).
proof: Proof. simple induction M; simpl in |- *; intros; auto with coc core arith sets. elim (le_gt_dec k n); elim (le_gt_dec i n); intros. rewrite lift_ref_ge; auto with coc core arith sets. rewrite lift_ref_ge; auto with coc core arith sets. elim plus_assoc_reverse with p n0 n. elim plus_assoc_reverse with n0 p n. elim plus_comm with p n0; auto with coc core arith sets. apply le_trans with n; auto with coc core arith sets. absurd (i <= n); auto with coc core arith sets. apply le_trans with k; auto with coc core arith sets. rewrite lift_ref_ge; 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 lift_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. rewrite plus_n_Sm; 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. rewrite plus_n_Sm; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations