proposition: Lemma Ered1_subst_l : forall (a t u : term) (k : nat), Ered1 t u -> Ered (subst_rec t a k) (subst_rec u a k).
proof: Proof. simple induction a; simpl in |- *; auto with ecoc coc core arith sets. intros. elim (lt_eq_lt_dec k n); [ intro a0 | intro b; auto with ecoc coc core arith sets ]. elim a0; auto with ecoc coc core arith sets. unfold lift in |- *; auto with ecoc coc core arith sets. Qed.
imports: Termes Conv