proposition: Lemma subst_ref_gt : forall u n k, n > k -> subst_rec u (Ref n) k = Ref (pred n).
proof: Proof. simpl in |- *; intros. elim (lt_eq_lt_dec k n); [ intro a | intro b ]. elim a; clear a; [ intro a; auto with coc core arith sets | intro b ]. inversion_clear b in H. elim gt_irrefl with n; auto with coc core arith sets. absurd (k <= n); auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations