proposition: Lemma inv_conv_prod_r : forall a b c d : term, conv (Prod a c) (Prod b d) -> conv c d.
proof: Proof. intros. elim church_rosser with (Prod a c) (Prod b d); intros; auto with coc core arith sets. apply red_prod_prod with a c x; intros; auto with coc core arith sets. apply red_prod_prod with b d x; intros; auto with coc core arith sets. apply trans_conv_conv with b0; auto with coc core arith sets. apply sym_conv. generalize H2. rewrite H5; intro. injection H8. simple induction 1; auto with coc core arith sets. Qed.
imports: Termes