small comment
cp dev/ip-pr-muDot.v dev/cbounds-ip-pr-muDot.v
introduce cbounds judgment ("type contains recursively contains only collapsed type member bounds")
cbounds updates
define cbounds_ctx