formal: complete reachable Phase-1 TODOs for project/limit and redundant-project theorem#1424

SkBlaz merged 2 commits into

masterSkBlaz/py3plex:masterfrom

copilot/formal2-go-over-todosSkBlaz/py3plex:copilot/formal2-go-over-todosCopy head branch name to clipboard