Added distributitivity laws for separating conjunction to BILogic.v