proposition: Lemma eqE (b1 b2 : UM.base C V) : to b1 = to b2 :> U <-> b1 = b2.
proof: Proof. by split=>[E|-> //]; rewrite -[b1]ftE -[b2]ftE E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)