proposition: Lemma inv_Econv_prod_r : forall a b c d : term, Econv (Prod a c) (Prod b d) -> Econv c d.
proof: Proof. intros. elim Econv_church_rosser with (Prod a c) (Prod b d); intros; auto with ecoc coc core arith sets. apply Ered_prod_prod with a c x; intros; auto with ecoc coc core arith sets. apply Ered_prod_prod with b d x; intros; auto with ecoc coc core arith sets. apply trans_Econv_Econv with b0; auto with ecoc coc core arith sets. apply sym_Econv. generalize H2. rewrite H5; intro. injection H8. simple induction 1; auto with ecoc coc core arith sets. Qed.
imports: Termes Conv