proposition: Theorem wf_ord_norm : forall t : term, sn t -> Acc ord_norm t.
proof: Proof. unfold ord_norm in |- *. intros. apply Acc_clos_trans. apply wf_ord_norm1; auto with coc sets. Qed.
imports: Peano_dec Transitive_Closure Union Termes Conv