iff/equivalence vs preservation + reflection?
Status: open (writing decision)
How should the correctness theorem be stated: as a full iff / typability-equivalence between the double-vision rule and the single-vision encoding, or more conservatively as preservation + reflection of the obligations (premises 5/6)?
What would settle it
Decide which statement the paper can actually justify; a conservative typability-equivalence paragraph for premises (5)/(6) was the immediate writing target.
Related
Source-to-Source Encoding Correctness · Double-Vision Recursive Modules