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