correctness and beta-coherence can be rolled up into one specific property
Is that rolling up two things into one, or is that just beta-coherence?
Is that rolling up two things into one, or is that just beta-coherence?