add lemmas for 'separable' propositions
I also had to move the 'pure' lemmas down so that we can have "pure is separable" in that section.
This paves the ground for !843 (closed).
I also had to move the 'pure' lemmas down so that we can have "pure is separable" in that section.
This paves the ground for !843 (closed).