proposition: Lemma ext_clP cl1 th k v (cl1k := (cl1.1, (k, v) :: cl1.2)) : cl1 \in th -> exists2 th1, ext_cl th cl1 k v = Wrap th1 & cl1k \in th1 /\ th1 =i [pred cl | if cl.1 == cl1.1 then cl == cl1k else cl \in th].
proof: Proof. case: cl1 => ij kvs /= in cl1k * => th_cl1; set th1p := [pred cl | _]. pose th1 := [seq (if cl.1 == ij then cl1k else cl) | cl <- th]. exists th1; first by elim: (th) @th1 => //= cl th' ->; rewrite -2!fun_if. suffices Dth1: th1 =i th1p by rewrite Dth1 !inE !eqxx. move=> cl; rewrite inE; apply/mapP/idP=> [[{}cl th_cl ->] | ]. by case cl_ij: (cl.1 == ij); rewrite ?eqxx ?cl_ij. case: ifP => [_ /eqP-> | cl'ij th_cl]; last by exists cl; rewrite ?cl'ij. by exists (ij, kvs); rewrite ?eqxx. 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)