proposition: Lemma Epar_red1_lift : forall (n : nat) (a b : term), Epar_red1 a b -> forall k : nat, Epar_red1 (lift_rec n a k) (lift_rec n b k).
proof: Proof. simple induction 1; simpl in |- *; eauto with coc ecoc core arith sets. intros. rewrite distr_lift_subst; auto with coc ecoc core arith sets. Qed.
imports: Termes Conv