proposition: Lemma sat_cases (m : model) th k cl : sat m th -> cl \in th -> wf_ext_cl cl k (size m) -> exists2 v, v \in lit_vals & sat m (unwrap (ext_cl th cl k v)).
proof: Proof. case: cl => ij kvs /satP thP th_cl /andP[cl'k ltkm]. have [[_ ZmL _] [o1m ZmR]] := (LmodelP m, RmodelP m). have [m_ij Uij clP] := thP _ th_cl. have /CintP[v Dv]: '[m ij, m`_k] \in Cint. by rewrite Cint_cfdot_vchar ?ZmL ?ZmR ?mem_nth. have [/= th1 Dthx [th1_cl Dth1]] := ext_clP k v th_cl. suffices{Dthx} m_th1: sat m th1. exists v; last by rewrite /ext_cl Dthx. by case: (v) (norm_lit m_th1 th1_cl (mem_head _ _)); do 2?case. apply/satP=> cl1; rewrite Dth1 inE; case: ifP => [_ /eqP-> | _ /thP] //=. by rewrite cl'k; split=> // kv /predU1P[-> | /clP//]; rewrite /sat_lit Dv. 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)