proposition: Lemma In_umcomp g f k v : (k, v) \In um_comp g f <-> valid (um_comp g f) /\ exists k', (k, k') \In f /\ (k', v) \In g.
proof: Proof. split=>[H|[W][k'][]]. - split; first by case: H. elim/um_indf: f H=>[||x w f IH P W]. - by rewrite umcomp_fundef=>/In_undef. - by rewrite umcompf0=>/In0. rewrite /um_comp umfoldlUn_frame //; last by move=>*; case: (find _ _)=>// a; rewrite joinA. rewrite unitR !umfoldlPt; case: ifP=>C; last first. - by rewrite undef_join=>/In_undef. case/InUn; last by case/IH=>k' [H1 H2]; exists k'; split=>//; apply/InR. case E: (find _ _)=>[b|]; last by move/In0. rewrite unitR=>/InPt; case; case=>?? _; subst x b. by exists w; split=>//; apply/In_find. elim/um_indf: f W k'=>[||x w f IH P W] W' k'. - by move/In_undef. - by move/In0. rewrite umcompfPtUn // in W'; rewrite InPtUnE //. case=>[[??] G|H1 H2]. - subst x w; rewrite umcompfPtUn //. by move/In_find: (G)=>E; rewrite E in W' *; apply/InPtUnL. rewrite umcompfPtUn //. case E: (find _ _) W'=>[b|] W'; last by apply: IH H1 H2. by apply/InR=>//; apply:IH H1 H2; rewrite (validR W'). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)