Includes bringing some of the predicate logic section into closer alignment with set.mm (mostly theorems used by fprod2d).
The proofs of most of the finite product theorems are via finite set induction (without the need to expand to an expression involving seq). Others are basically the set.mm proofs with some intuitionizing.
Includes bringing some of the predicate logic section into closer alignment with set.mm (mostly theorems used by fprod2d).
The proofs of most of the finite product theorems are via finite set induction (without the need to expand to an expression involving
seq). Others are basically the set.mm proofs with some intuitionizing.