proposition: Lemma isc_rel_class2 u: inc u (source f) -> nonempty (Vf f u) -> classp (partition_relation f x) (Vf f u) .
proof: Proof. move=> us neW. move: isc_rel_equivalence => ec. rewrite (proj33 ff) in us. have sWx: (sub (Vf f u) x) by rewrite -(proj33 fpa) => t tW; union_tac. move: (rep_i neW) => rw;move: (sWx _ rw) => rs. move:(cover_at_pr fpa us rw) => pa. hnf; rewrite isc_rel_sr //; split=> //. set_extens t. 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);rewrite pa. move /(class_P ec) /isc_rel_P => h; move: (proj2 (isc_hi h)) => tx. rewrite -pa; move: (proj1 (cover_at_in fpa tx)). by move /(isc_rel1P rs tx): h => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)