Add basic lemmas to exploit hypotheses in behavior

This ensures all hypotheses in behavior have corresponding trivial lemmas in analysis/facts/all that enable to exploit them. This also makes the code more robust to potential changes in the precise way these hypotheses are stated.