proposition: Lemma subst_ref_eq : forall u n, subst_rec u (Ref n) n = lift n u.
proof: Proof. intros; simpl in |- *. elim (lt_eq_lt_dec n n); [ intro a | intro b ]. elim a; intros; auto with coc core arith sets. elim lt_irrefl with n; auto with coc core arith sets. elim gt_irrefl with n; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations