proposition: Lemma all_supp_insP (k : K) v : C k -> all C (supp f) -> all C (supp (ins k v f)).
proof: Proof. move=>H1 H2; apply/allP=>x; rewrite supp_ins inE /=. by case: eqP=>[->|_] //=; move/(allP H2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)