module language/theorems
assert DotAssociative {
	all p, q, r: univ -> univ | (p.q).r = p.(q.r)
	}
check DotAssociative
assert BadUnionRule {
	all p, q, r: univ -> univ | p = q+r  iff p-q = r
	}
check BadUnionRule