Read rule QED.
All rules proven. While and assn_sub done in this commit.