Adapting FiniteType to support constructors with multiple arguments

[maxkurze1]

It took me a while, but I figured out the problems of my first approach (see #2).

I turned out that finite_surjective was used as part of computations which get stuck once they encounter an opaque term/lemma. So the solution was basically to redefine all lemma dependencies using nothing than transparent terms.

Now, we can finally derive FiniteType type classes for more complex (possibly even all finite) Inductive types.

[spacefrogg]

You've created a dependency cycle (have a look at the CI output).

[maxkurze1]

Oh, I am sorry for bothering you, that commit is still a WIP. I just wanted to have it persisted in git. I didn't quite remember there was already a PR for this branch. Anyway; you can notice these commits by their meaningless commit names ^^. Have a nice day.