We show that R is a hidden -congruence.
We use quantifier elimination, implication elimination, and reduction to show that
(F1, F2 : Flag) F1 R F2   implies   (up? F1) R (up? F2) .
This involves the following steps:
  1. introduce new constants f1, f2 of sort Flag ;
  2. assume f1 R f2 = true ;
  3. show (up? f1) R (up? f2) = true by reduction.

26 September 26 1996