proposition: Lemma red_prod_prod : forall u v t, red (Prod u v) t -> forall P : Prop, (forall a b : term, t = Prod a b -> red u a -> red v b -> P) -> P.
proof: Proof. simple induction 1; intros. apply H0 with u v; auto with coc core arith sets. apply H1; intros. inversion_clear H4 in H2. inversion H2. apply H3 with N1 b; auto with coc core arith sets. apply trans_red with a; auto with coc core arith sets. apply H3 with a N2; auto with coc core arith sets. apply trans_red with b; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations