proposition: Lemma subterm_sn : forall a : term, sn a -> forall b : term, subterm b a -> sn b.
proof: Proof. unfold sn in |- *. simple induction 1; intros. apply Acc_intro; intros. elim commut_red1_subterm with x b y; intros; auto with coc core arith sets. apply H1 with x0; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations