“By using Dec, you’ve been able to write explicitly in the type what checkEqNat is supposed to do: run either a proof that the inputs are equal, or a proof that they’re not.”