proposition: Lemma lift_ref_lt : forall k n p, p > n -> lift_rec k (Ref n) p = Ref n.
proof: Proof. intros; simpl in |- *. elim (le_gt_dec p n); auto with coc core arith sets. intro; absurd (p <= n); auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations