proposition: Lemma simpl_subst : forall N M n p, p <= n -> subst_rec N (lift (S n) M) p = lift n M.
proof: Proof. intros; unfold lift in |- *. apply simpl_subst_rec; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations