proposition: Lemma par_red1_lift : forall n (a b : term), par_red1 a b -> forall k, par_red1 (lift_rec n a k) (lift_rec n b k).
proof: Proof. simple induction 1; simpl in |- *; auto with coc core arith sets. intros. rewrite distr_lift_subst; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations