proposition: Lemma Ered1_Ered_ind : forall (N : term) (P : term -> Prop), P N -> (forall M R : term, Ered1 M R -> Ered R N -> P R -> P M) -> forall M : term, Ered M N -> P M.
proof: Proof. cut (forall M N : term, Ered M N -> forall P : term -> Prop, P N -> (forall M R : term, Ered1 M R -> Ered R N -> P R -> P M) -> P M). intros. apply (H M N); auto with ecoc coc core arith sets. simple induction 1; intros; auto with ecoc coc core arith sets. apply H1; auto with ecoc coc core arith sets. apply H4 with N0; auto with ecoc coc core arith sets. intros. apply H4 with R; auto with ecoc coc core arith sets. apply Etrans_red with P; auto with ecoc coc core arith sets. Qed.
imports: Termes Conv