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