proposition: Lemma lift_ref_ge : forall k n p, p <= n -> lift_rec k (Ref n) p = Ref (k + 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