page 2  1 2 3 4 
Associativity of union
We want to prove ( S0 S1 S2 : Set ) (S0 U S1) U S2 = S0 U (S1 U S2) . This goal is proved directly by circular coinductive rewriting.
Commutativity of union We want to prove ( S0 S1 : Set ) S0 U S1 = S1 U S0 . This goal is proved directly by circular coinductive rewriting.
Idempotency of union We want to prove ( S : Set ) S U S = S . This goal is proved directly by circular coinductive rewriting.
The empty set is a unit for union We want to prove ( S : Set ) empty U S = S . 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.)

