Perfect, that worked. There is no educational reason, I am just a beginner that didn't know lia existed.

I was able to solve the original problem with induction tactic over Sd_dec m but I think an answer could still be interesting and valuable learning.

I understand now how sumbool would interact with match, but how that that work with if?

Also, I don't understand what is going on with cd_dec here. It looks like a definition to tell that law of excluded middle holds for Cd (actually, that it's either provable or disprovable I guess), but then it's instantiated and supposed to be the decidable version of Cd? How does that work?

Thanks, I understand now the issue with decidability, I think (although I am not certain why the proof system needs to care about decidability). All my stuff is trivially decidable though, I know the values at every t.

@AndrejBauer Whoops, thanks.

So, if I have excluded middle (this is what propositions being decidable means, right?), the easiest for reasoning is your first example? I just want a nicer replacement for the hypotheses I currently use to define delay, but if the replacement is more awkward I can also stick with those.

@MevenLennon-Bertrand Fair, fixed.

@MevenLennon-Bertrand Added the variable declarations, there is nothing else relevant between those and the Fixpoint definition.