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:
introduce a new
constant
f
of sort
Flag
.
introduce
the
lemma
(
B : Bool) not not B = B
.
show
(rev rev f) R f = true
by
reduction
.
13 October 1996