Confusion between prop and bool in F*

[gebner]

C2pulse maps some terms of type bool to Fs bool (like equality, comparisons) and others to F (quantifiers, implication). Sadly F* doesn't reliably coerce between the two, so you get some errors e.g. when you nest a quantifier in a boolean expression.

Option 1: map everything to bool, insert strong_excluded_middle around forall/implication

Option 2: add a _specprop type that corresponds to F*s prop, and emit casts as b2t and strong_excluded_middle.