fix(tactic/derive_fintype): add support for props (#4777)
This adds support for propositional arguments in inductive constructors.
It was previously not handled, and while it *almost* works without
change, we have to use `Sigma' (a:A) (b:B) (c:C), unit` to tuple up the
arguments instead of `Sigma' (a:A) (b:B), C` because it would cause problems
in the unary case where there is only one propositional field.
