proposition: Lemma th_bboxP th bb : reflect {in th, forall cl, cl.1 \in wf_ref bb} (sub_bbox (th_bbox th) bb).
proof: Proof. pose in_bb := [pred cl : clause | cl.1 \in wf_ref bb]. suffices ->: sub_bbox (th_bbox th) bb = all in_bb th by apply: allP. elim: th => [|[[i j] _] th] //=; case: (th_bbox th) => ri rj /=. by rewrite /sub_bbox /= !geq_max andbACA => ->. 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)