(∃ v . e ⇒ v) ⇔ (∃ v′ ~ v . [[e]] ⇒ v′)except that the scope doesn't work out: v is only in scope in the first parenthesized proposition, so it can't be referred to in the second one. Of course, it's generally sufficient to prove co-termination and just leave out the relationship between the final values, since that's usually easily derivable. But it's an important part of the intuition behind correctness, so I want the relationship between answers to be in the statement of the theorem.
An awkward way to make this work is to write big clunky conjunctions like:
(e⇓ ⇔ [[e]]⇓) ∧ (∀ v . e ⇒ v . ∃ v′ ~ v . [[e]] ⇒ v′)But it would be nice if there were some way to write it more compactly like the first pseudo-proposition I wrote. I like that it reads almost like you'd say in English: "e and [[e]] always get the same answers."
Anyone have any suggestions?
