Lists in product and sigma types #
This file proves basic properties of list.product
and list.sigma
, which are list constructions
living in prod
and sigma
types respectively. Their definitions can be found in
data.list.defs
. Beware, this is not about list.prod
, the multiplicative product.