proposition: Lemma sn_prod : forall A, sn A -> forall B, sn B -> sn (Prod A B).
proof: Proof. unfold sn in |- *. simple induction 1. simple induction 3; intros. apply Acc_intro; intros. inversion_clear H5; auto with coc core arith sets. apply H1; auto with coc core arith sets. apply Acc_intro; auto with coc core arith sets. Qed.
imports: Arith Compare_dec Relations