proposition: Lemma conv_conv_prod : forall a b c d : term, conv a b -> conv c d -> conv (Prod a c) (Prod b d).
proof: Proof. intros. apply trans_conv_conv with (Prod a d). elim H0; intros; auto with coc core arith sets. apply trans_conv_red with (Prod a P); auto with coc core arith sets. apply trans_conv_exp with (Prod a P); auto with coc core arith sets. elim H; intros; auto with coc core arith sets. apply trans_conv_red with (Prod P d); auto with coc core arith sets. apply trans_conv_exp with (Prod P d); auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations