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:
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