module joins
assert A {
	all s: set univ, r: univ -> univ |
		let iden3 = {a, b, c: univ | a = b and b = c} |
			s.iden3.r = s <: r
			and 
			r.iden3.s = r :> s
	}
check A for 6

assert B {
	all r: univ -> univ |
		~r in r iff ~r = r
	}
check B for 6