proposition: Lemma pmap_pcomp {S T U} (f : T -> option U) (g : S -> option T) s : pmap (pcomp f g) s = pmap f (pmap g s).
proof: Proof. by elim: s=>//= x s ->; rewrite /pcomp; case: (g x). Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)