proposition: Lemma par_red1_subst : forall c d : term, par_red1 c d -> forall a b : term, par_red1 a b -> forall k, par_red1 (subst_rec a c k) (subst_rec b d k).
proof: Proof. simple induction 1; simpl in |- *; auto with coc core arith sets; intros. rewrite distr_subst; auto with coc core arith sets. elim (lt_eq_lt_dec k n); auto with coc core arith sets; intro a0. elim a0; intros; auto with coc core arith sets. unfold lift in |- *. apply par_red1_lift; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations