Add proofs on truth value

[mildsunrise]

Adds a handful of "congruence" proofs on the truth value of a decidable, and also ≐?:

• Relation.Nullary.Decidable:

  • does-≡: decidables over the same type have the same truth value
  • does-⇔: generalization of does-≡ to mutually implied types

• Relation.Unary.Properties:

  • ≐?: generalization of Decidable.map to predicates (if two predicates are equivalent, one is decidable if the other is)
  • does-≡: generalization of does-≡ to predicates
  • does-≐: generalization of does-⇔ to predicates

Using these, together with the definitions in Decidable.Core, one can prove the effect of type operations on truth value. For example, proving that Dec (¬ A) and Dec A have negated truth values can be done as does-≡ ¬a? (¬? a?). Same with × / ∧ and ⊎ / ∨.

[mildsunrise]

(I've simplified the proofs, but the statements remain unchanged)

[MatthewDaggitt]

@JacquesCarette are you willing to approve now?