proposition: Lemma pcm51_morph_ax : morph_axiom (@sepT (prod5_PCM U1 U2 U3 U4 U5)) pcm51.
proof: Proof. by split=>[|x y]; rewrite !pcmE /= !pcmE //= =>/and4P []. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)