proposition: Lemma subst_rec_Ered1_r : forall N M M' : term, Ered1 M M' -> forall k : nat, Ered1 (subst_rec N M k) (subst_rec N M' k).
proof: Proof. simple induction 1; simpl in |- *; intros; auto with ecoc. rewrite distr_subst. auto with ecoc. Qed.
imports: Termes Conv