fact: Fixpoint sat gT vT B n (s : vT -> env gT) p := match p with | Formula f => [exists v, let: Env A e := s v in and_rel A B (rel (rev e) f NoRel)] | Generator p' => let s' v := let: Env A e := s v.1 in Env (A <*> <[v.2]>) (v.2 :: e) in sat B n.+1 s' (p' (Cst n)) end.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq) mathcomp(fintype finset fingroup morphism)