proposition: Lemma red_par_red : forall M N, red M N -> par_red M N.
proof: Proof. red in |- *; simple induction 1; intros; auto with coc core arith sets. apply t_trans with P; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations