proposition: Lemma Econv_Econv_subst : forall (a b c d : term) (k : nat), Econv a b -> Econv c d -> Econv (subst_rec a c k) (subst_rec b d k).
proof: Proof. intros. apply trans_Econv_Econv with (subst_rec a d k). elim H0; intros; auto with ecoc coc core arith sets. apply Etrans_conv_red with (subst_rec a P k); auto with ecoc coc core arith sets. apply Etrans_conv_exp with (subst_rec a P k); auto with ecoc coc core arith sets. elim H; intros; auto with ecoc coc core arith sets. apply trans_Econv_Econv with (subst_rec P d k); auto with ecoc coc core arith sets. apply trans_Econv_Econv with (subst_rec P d k); auto with ecoc coc core arith sets. apply sym_Econv; auto with ecoc coc core arith sets. Qed.
imports: Termes Conv