page 3  1 2 3 x 
Finally we show
(rev rev F) R F
.
We want to prove ( F : Flag ) (rev (rev F)) R F .We take the following steps:
And thus the main goal is proved. 
Explanation
1. Because the formula to be proved is universally quantified, our first step is to eliminate the quantifier, by introducing a new constant, f of sort Flag, to stand for the variable F . 2. After adding "= true " as its right side, and substituting f for F, what remains to be proved is the equation (rev rev f R f) = true .For this, we use reduction, applying the current set of rewrite rules to each side, to see if these two terms reduce to the same thing, which they do. 
