proposition: Lemma unsat_cases th ij kvs tO : is_sat_test tO -> oapp (unsat_cases_hyp th kvs tO) False (get_cl ij th) -> unsat th.
proof: Proof. case: get_clP => //= cl [th_cl _] O; rewrite /unsat_cases_hyp. case: head => k _; set thk_ := ext_cl th cl k; set add := fun _ _ => _. set wf_kvs := _ && _; rewrite -[kvs]revK foldl_rev => Ukvs m m_th. have{Ukvs}: all (fun kv => ~~ sat m (unwrap (thk_ kv.2))) (rev kvs) && wf_kvs. elim: rev Ukvs => // [[_ v] /= kvs' IH]; case Dthk: (thk_ v) => [thv] [/IH]. by rewrite -andbA => -> Uthk; rewrite andbT; apply/negP; apply: Uthk. case/and3P=> /allP Uthkvs /andP[cl'k ltkr] /allP Uthkv's. have [|{cl'k ltkr} v lit_v m_thv] := sat_cases k m_th th_cl. by rewrite /wf_ext_cl cl'k (leq_trans ltkr) //; have [] := and3P m_th. have /idPn[] := O _ _ m_thv; apply: Uthkv's; apply: map_f. rewrite mem_filter lit_v andbT -mem_rev -map_rev. by apply: contraL m_thv => /mapP[kv /Uthkvs m'thkv ->]. Qed.
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)