proposition: Lemma distr_subst : forall (P : term) N M k, subst_rec P (subst N M) k = subst (subst_rec P N k) (subst_rec P M (S k)).
proof: Proof. intros; unfold subst in |- *. pattern k at 1 3 in |- *. replace k with (0 + k); auto with coc core arith sets. apply distr_subst_rec. Qed.
imports: Arith Compare_dec Relations