proposition: Lemma lift_rec0 : forall M k, lift_rec 0 M k = M.
proof: Proof. simple induction M; simpl in |- *; intros; auto with coc core arith sets. elim (le_gt_dec k n); auto with coc core arith sets. rewrite H; rewrite H0; auto with coc core arith sets. rewrite H; rewrite H0; auto with coc core arith sets. rewrite H; rewrite H0; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations