fact: Fixpoint holds (e : seq R) (f : ord.formula R) {struct f} : Prop := match f with | Bool b => b | (t1 == t2)%oT => eval e t1 = eval e t2 | (t1 <% t2)%oT => eval e t1 < eval e t2 | (t1 <=% t2)%oT => eval e t1 <= eval e t2 | Unit t1 => eval e t1 \in unit | (f1 /\ f2)%oT => holds e f1 /\ holds e f2 | (f1 \/ f2)%oT => holds e f1 \/ holds e f2 | (f1 ==> f2)%oT => holds e f1 -> holds e f2 | (~ f1)%oT => ~ holds e f1 | ('exists 'X_i, f1)%oT => exists x, holds (set_nth 0 e i x) f1 | ('forall 'X_i, f1)%oT => forall x, holds (set_nth 0 e i x) f1 end.
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)