proposition: Lemma red1_subst_l : forall (a : term) t u k, red1 t u -> red (subst_rec t a k) (subst_rec u a k).
proof: Proof. simple induction a; simpl in |- *; auto with coc core arith sets. intros. elim (lt_eq_lt_dec k n); [ intro a0 | intro b; auto with coc core arith sets ]. elim a0; auto with coc core arith sets. unfold lift in |- *; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations