proposition: Lemma isc_rel_class a: classp (partition_relation f x) a -> exists2 u, inc u (source f) & a = Vf f u.
proof: Proof. move=> [rs ac]. move: isc_rel_equivalence => ec. rewrite isc_rel_sr in rs. move: (cover_at_in fpa rs); set u := cover_at _ _;move => [pa pb]. rewrite ac /Vf (proj33 ff); ex_tac. set_extens t. move /(class_P ec) /isc_rel_P => h; move: (proj2 (isc_hi h)) => tx. by move: (cover_at_in fpa tx)=> []; move /(isc_rel1P rs tx): h => <-. move => ts. have tx: inc t x by rewrite - (proj33 fpa); union_tac. apply /(class_P ec) /isc_rel_P /(isc_rel1P rs tx). by symmetry; apply:(same_cover_at fpa rs ts). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)