proposition: Lemma simpl_lift_rec : forall M n k p i, i <= k + n -> k <= i -> lift_rec p (lift_rec n M k) i = lift_rec (p + 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 lift_ref_ge; auto with coc core arith sets. rewrite plus_comm; apply le_trans with (k + n0); 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; simpl in |- *; auto with coc core arith sets. rewrite H; auto with coc core arith sets; rewrite H0; simpl in |- *; auto with coc core arith sets. rewrite H; auto with coc core arith sets; rewrite H0; simpl in |- *; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations