I am trying to have some lemmas with (P: T1 -> Prop) and (R: T1 -> T2 -> Prop) and some of those lemmas also assume that P and Q should be decidable, which kind of means P and Q can be refleced to functions that return bool, but I wanted to know what would be the correct pattern to have those assumptions ?

Lemmas usually have to flavors:

1- if `P x is decidable`

then `map P some_data_structure followed by and-ing all the results is also decidable`

2- not custom_forall x, P x<-> custom_exists y, ~ P y.

Last updated: Feb 08 2023 at 07:02 UTC