Added more core lemmas to ILogic and BILogic.
Added support to prove that any embedding of Prop into a BILogic is
pure.

Note that currently the Pure type class only works for intuitionistic
separation logics.