proposition: Lemma pi_CD (x y : C) : reflect (pi x = pi y) (eC x y).
proof: Proof. apply: (iffP idP) => hxy. apply: (can_inj ereprK); unlock pi canon => /=. rewrite -(@eq_choose _ (eC x) (eC y)); last first. by move=> z; rewrite /eC /=; apply: equiv_ltrans. by apply: choose_id; rewrite ?equiv_refl //. rewrite (equiv_trans (chooseP (equiv_refl _ _))) //=. move: hxy => /(f_equal erepr) /=; unlock pi canon => /= ->. by rewrite equiv_sym /= chooseP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice) mathcomp(seq fintype)