proposition: Lemma umcomp_undeff f : valid f -> um_comp undef f = Unit.
proof: Proof. move=>W; apply: (umfoldl_ind (P:=fun r => r = Unit))=>//. by move=>*; rewrite find_undef. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)