proposition: Lemma Econv_Econv_lift : forall (a b : term) (n k : nat), Econv a b -> Econv (lift_rec n a k) (lift_rec n b k).
proof: Proof. intros. elim H; intros; auto with ecoc coc core arith sets. apply Etrans_conv_red with (lift_rec n P k); auto with ecoc coc core arith sets. apply Etrans_conv_exp with (lift_rec n P k); auto with ecoc coc core arith sets. Qed.
imports: Termes Conv