proposition: Lemma isc_rel_equivalence: equivalence (partition_relation f x).
proof: Proof. apply: equivalence_from_rel; split. by move => u v [i [isf Wx Wy]]; exists i. move => b a c pa pb. move: (isc_hi pa) (isc_hi pb) => [ax bx] [_ cx]. apply/(isc_rel1P ax cx). by move /(isc_rel1P ax bx): pa => ->; move /(isc_rel1P bx cx): pb => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)