psigma.fintype_prop_left source