Experiment with correctness proof
Re-introduce version with more precise AEnv
Checkpoint correctness
Work on correctness
Promising attmpt at a correctness proof
Cleanup