proposition: Lemma equivQTP : cancel (CD \o erepr) (pi \o DC).
proof: Proof. by move=> x; rewrite /= (pi_CD _ (erepr x) _) ?ereprK /eC /= ?encDP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice) mathcomp(seq fintype)