[Hol-info] Question about Type (:M+N) in HOL Light

Hi, everyone. I know the type :(M,N)finite_sum in library "Definition of finite Cartesian product types". What is the difference between (:M+N) and :(M,N)finite_sum? Is there the theorem |- dimindex (:M+N) = dimindex(:M)+dimindex(:N) in the existing library? Thank you very much. Best

[Hol-info] SAT/SMT/AR Summer School 2018

[Apologise for cross-posting. Please forward to anybody you think may be interested] SAT/SMT/AR Summer School 2018 University of Manchester, 3-6th July