fact: Fixpoint rformula (f : formula R) := match f with | Bool _ => true | t1 == t2 => rterm t1 && rterm t2 | t1 <% t2 => rterm t1 && rterm t2 | t1 <=% t2 => rterm t1 && rterm t2 | Unit t1 => false | (f1 /\ f2) | (f1 \/ f2) | (f1 ==> f2) => rformula f1 && rformula f2 | (~ f1) | ('exists 'X__, f1) | ('forall 'X__, f1) => rformula f1 end%oT.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div choice fintype) mathcomp(bigop order ssralg finset fingroup zmodp) mathcomp(poly ssrnum)