proposition: Lemma pi_DC (x y : D) : reflect (pi (DC x) = pi (DC y)) (eD x y).
proof: Proof. apply: (iffP idP)=> hxy. apply/pi_CD; rewrite /eC /=. by rewrite (equiv_ltrans (encDP _)) (equiv_rtrans (encDP _)) /= encDE. rewrite -encDE -(equiv_ltrans (encDP _)) -(equiv_rtrans (encDP _)) /=. exact/pi_CD. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice) mathcomp(seq fintype)