proposition: Lemma red1_red_ind : forall N (P : term -> Prop), P N -> (forall M (R : term), red1 M R -> red R N -> P R -> P M) -> forall M, red M N -> P M.
proof: Proof. cut (forall M N, red M N -> forall P : term -> Prop, P N -> (forall M (R : term), red1 M R -> red R N -> P R -> P M) -> P M). intros. apply (H M N); auto with coc core arith sets. simple induction 1; intros; auto with coc core arith sets. apply H1; auto with coc core arith sets. apply H4 with N0; auto with coc core arith sets. intros. apply H4 with R; auto with coc core arith sets. apply trans_red with P; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations