proposition: Lemma dom0NP f : reflect (exists k, k \in dom f) (dom f != [::]).
proof: Proof. case: has_nilP=>X; constructor. - by case/hasP: X=>x; exists x. by case=>k D; apply: X; apply/hasP; exists k. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)