proposition: Lemma um_indb (P : U -> Prop) : P undef -> P Unit -> (forall k v f, P f -> valid (f \+ pts k v) -> (forall x, x \in dom f -> ord x k) -> P (pts k v \+ f)) -> forall f, P f.
proof: Proof. rewrite !pcmE /undef /= !umEX => H1 H2 H3 f; rewrite -[f]UMC.tfE. apply: (UM.base_indb (P := (fun b => P (UMC.to b))))=>//. move=>k v g H V1; move: (H3 k v _ H); rewrite !pcmE /= !umEX. by apply. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)