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