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: Oct 13 2024 at 01:02 UTC