proposition: Lemma sn_subst : forall T M, sn (subst T M) -> sn M.
proof: Proof. intros. cut (forall t, sn t -> forall m : term, t = subst T m -> sn m). intros. apply H0 with (subst T M); auto with coc core arith sets. unfold sn in |- *. simple induction 1; intros. apply Acc_intro; intros. apply H2 with (subst T y); auto with coc core arith sets. rewrite H3. unfold subst in |- *; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations