proposition: Lemma red1_subst_r : forall t u, red1 t u -> forall (a : term) k, red1 (subst_rec a t k) (subst_rec a u k).
proof: Proof. simple induction 1; simpl in |- *; intros; auto with coc core arith sets. rewrite distr_subst; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations