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