page 1  1 2 3 x 
We show that reversing a flag twice has no effect.
We want to prove ( F : Flag ) rev (rev F) = F .We use explicit coinduction to prove that it is a behavioral property of the input specification. For this, we use the following:

Explanation
This coinduction proof, like many others, uses a default selection of the cobasis. This makes some parts of the proof automatic. Because R is the identity on visible sorts, we need only show the congruence property for
the (single) operation in ; this explains the single formula to be proved on this
tatami.

