proposition: Lemma Ered1_subst_r : forall t u : term, Ered1 t u -> forall (a : term) (k : nat), Ered1 (subst_rec a t k) (subst_rec a u k).
proof: Proof. simple induction 1; simpl in |- *; intros; auto with ecoc coc core arith sets. rewrite distr_subst; auto with ecoc coc core arith sets. Qed.
imports: Termes Conv