proposition: Lemma encoded_equiv_is_equiv : equiv_class_of e'.
proof: Proof. split => [x|x y|y x z]; rewrite !e'E //=; first by rewrite equiv_sym. by move=> exy /(equiv_trans exy). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice) mathcomp(seq fintype)