proposition: Lemma induced_rel_classP x: (classp (induced_relation r a) x <-> exists y, [/\ classp r y, nonempty (y \cap a) & x = (y \cap a)]).
proof: Proof. have iia:=(induced_rel_iirel_axioms). move: (ira)=> [er ar]. have p: forall y, Vfi (canonical_injection a (substrate r)) y = y \cap a. rewrite/Vfi /canonical_injection; aw. rewrite - diagonal_is_identity. move=> y;set_extens t. move /iim_graph_P => [u uy] /diagonal_pi_P [pa pb]; apply/setI2_P. split => //; ue. move /setI2_P => [ty ta]; apply /iim_graph_P; ex_tac. by apply /diagonal_pi_P. split. move/(iirel_classP iia); rewrite (ci_range ar); move => [y]; rewrite p. by move => [pa pb pc]; exists y. move => [y [cy ney xi]]; apply/(iirel_classP iia); exists y. split; [ done | by rewrite (ci_range ar) | by rewrite p ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)