proposition: Lemma red_red1_ord_norm : forall a b : term, red a b -> forall c : term, red1 b c -> ord_norm c a.
proof: Proof. red in |- *. simple induction 1; intros; auto with coc sets. apply t_trans with N; auto with coc sets. Qed.
imports: Peano_dec Transitive_Closure Union Termes Conv