Commit 2023-01-20 17:11 a5db36af

View on Github →

Feat: Port data.prod.tprod (#1464) Port of data.prod.tprod

Estimated changes

added theorem List.TProd.elim_mk
added theorem List.TProd.elim_of_mem
added theorem List.TProd.elim_of_ne
added theorem List.TProd.elim_self
added theorem List.TProd.ext
added theorem List.TProd.fst_mk
added theorem List.TProd.mk_elim
added theorem List.TProd.snd_mk
added def List.TProd
added theorem Set.elim_preimage_pi
added theorem Set.mk_preimage_tprod