proposition: Lemma um_ind' (P : U -> Prop) : P undef -> P Unit -> (forall k v f, P f -> valid (pts k v \+ f) -> P (pts k v \+ f)) -> forall f, P f.
proof: Proof. by move=>H1 H2 H3; apply: um_indf=>// k v f H4 H5 _; apply: H3. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)