proposition: Lemma resX U (V : tpcm) D (f : @morphism U V D) S x : 'res_S f x = if S x Unit then f x else undef.
proof: Proof. by []. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)