add Bool.elim

[maxsnew]

I.e., the dependent version of if_then_else_

[felixwellen]

I think a slightly better place for Bool.elim is Cubica.Data.Bool.Properties (unfortunately, we are not really consistent with this). That hopefully makes it also easier to solve name conflicts.

[maxsnew]

Fixed now, following @felixwellen 's suggestion

[laMudri]

Is there something to be said about signalling the order of the arguments? I guess it matters less for the dependent eliminator.

[maxsnew]

If we're going to go full bikeshed on this:

1. Having true first matches if_then_else_ which is the non-dependent version of the same function
2. Having false first would sort of match Nat.elim if we think false would correspond to 0 and true would correspond to 1.

I think having it match if_then_else_ is probably more intuitive and as you say the dependent type will turn most mistakes into type errors anyway. And I think calling it elim is good for consistency/discoverability because it matches Data.Sum/Data.Nat etc

[felixwellen]

I agree with the reasoning on the order and it looks all good to me -> merging soon.