We show (rev rev F) R F.
We use quantifier elimination, lemma introduction and reduction to show that
( F : Flag) (rev rev F) R F .
This involves the following steps:
  1. introduce a new constant f of sort Flag.
  2. introduce the lemma ( B : Bool) not not B = B .
  3. show (rev rev f) R f = true by reduction.

13 October 1996