proposition: Lemma trans_red_red : forall M N (P : term), red M N -> red N P -> red M P.
proof: Proof. intros. generalize H0 M H. simple induction 1; auto with coc core arith sets. intros. apply trans_red with P0; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations