proposition: Lemma wf_ord_norm1 : forall t : term, sn t -> Acc ord_norm1 t.
proof: Proof. unfold ord_norm1 in |- *. intros. apply Acc_union; auto with coc sets. exact commut_red1_subterm. intros. apply wf_subterm. Qed.
imports: Peano_dec Transitive_Closure Union Termes Conv