fact: Definition unsat_cases_hyp th0 kvs tO cl := let: (k, _) := head (2%N, 0) kvs in let thk_ := ext_cl th0 cl k in let th's := [seq unwrap (thk_ v) | v <- lit_vals & v \notin unzip2 kvs] in let add hyp kv := let: (_, v) := kv in let: Wrap th := thk_ v in hyp /\ unsat th in foldl add (wf_ext_cl cl k (th_dim th0) && all (predC tO) th's) kvs.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg matrix poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor center gproduct cyclic pgroup abelian frobenius) mathcomp(mxalgebra mxrepresentation vector falgebra fieldext galois) mathcomp(ssrnum rat algC algnum classfun character) mathcomp(integral_char inertia vcharacter) odd_order(PFsection1 PFsection2)