page 3  1 2 3 4 
Associativity of intersection
We want to prove ( S0 S1 S2 : Set ) (S0 & S1) & S2 = S0 & (S1 & S2) . This goal is proved directly by circular coinductive rewriting.
Commutativity of intersection We want to prove ( S0 S1 : Set ) S0 & S1 = S1 & S0 . This goal is proved directly by circular coinductive rewriting.
Idempotence of intersection We want to prove ( S : Set ) S & S = S . This goal is proved directly by circular coinductive rewriting.
The empty set is a zero for intersection We want to prove ( S : Set ) empty & S = empty . This goal is proved directly by circular coinductive rewriting. 
Explanation
Each proof is a straightforward application of circular coinductive rewriting (the special case of attribute coinduction is actually sufficient), using the specification SET . (By the way, the buttons labelled Left,
Right, Up, Down don't do anything because each proof is complete on its own
page.)

