Add propositional functions and CNF parameterized over lit/var types

[Vtec234]

Propositional functions are propositional formulas up to semantic equivalence.

@JamesGallicchio I thought about your question of whether we want to use this or { f: PropAssignment ν → Bool | dependsOnFinitelyManyVars f } as the mathematical model, in particular in cases where we have a function but don't want to construct a prop. formula. I think the two definitions should be equivalent, but the current one is easier to make because it doesn't require defining dependsOnFinitelyManyVars first (I will add that in a later PR). We can deal with the non-formula issue later by proving that any function depending on a finite amount of vars can be encoded as a formula, essentially by picking an ordering on the variables it depends on and then doing iterated Shannon expansions (or constructing a non-reduced OBDD, if you want).

EDIT: Well, to be fair this one requires defining PropForm whereas the latter one doesn't. Maybe the other one is better. Hmmmm..

EDIT 2: I tried the other definition, but it is impredicative and not as easy to prove facts about as quotiented syntax; so let's stick with the first one.

[JamesGallicchio]

For future self: another potential model is (S : Finset V) x' ((\forall v \in S, Bool) -> Bool)

I have not thought deeply about it. But it is nicely self contained, and can nicely express partial assignments.

[JamesGallicchio]

Ok, we are back down to 1 CNF type.

I specialized all the old code to ICnf, but most of it can be generalized once we have classes for "variables can be iterated over" and "variables can map to/from Nat".

Notably, I hijacked PropForm for input to the Tseitin implementation. This made some of the encoding less pretty, because we don't have notation for PropForms yet.

I wasn't sure whether to add back notation; the old notation frequently needed type annotations to disambiguate from Prop, which was a small headache.