fact: Fixpoint holds (e : seq R) (f : formula R) {struct f} : Prop := match f with | Bool b => b | (t1 == t2)%T => eval e t1 = eval e t2 | Unit t1 => eval e t1 \in unit | (f1 /\ f2)%T => holds e f1 /\ holds e f2 | (f1 \/ f2)%T => holds e f1 \/ holds e f2 | (f1 ==> f2)%T => holds e f1 -> holds e f2 | (~ f1)%T => ~ holds e f1 | ('exists 'X_i, f1)%T => exists x, holds (set_nth 0 e i x) f1 | ('forall 'X_i, f1)%T => forall x, holds (set_nth 0 e i x) f1 end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)