proposition: Lemma sat_exact m th1 th2 : sub_match th1 th2 -> sat m th2 -> sat m th1.
proof: Proof. move/allP=> s_th12 /satP th2P; apply/satP => cl1 /s_th12/hasP[cl2 th_cl2]. case: eqP => // <- s_cl12; have [wf_ij2 Ucl2 cl2P] := th2P _ th_cl2. split=> // [|kv /(mem_subseq s_cl12)/cl2P//]. by rewrite (subseq_uniq _ Ucl2) ?map_subseq. 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)