proposition: Lemma iirel_relatedP f r: iirel_axioms f r -> forall x y, (related (inv_image_relation f r) x y <-> [/\ inc x (source f), inc y (source f) & related r (Vf f x) (Vf f y)]).
proof: Proof. move=> ia. have fc : function ((canon_proj r) \co f) by apply: iirel_f. move: ia => [ff er tf]. rewrite /inv_image_relation. have cct: ((canon_proj r) \coP f) by split; aww. have iWs: forall u, inc u (source f) -> inc (Vf f u) (substrate r). by move=> u; rewrite tf; fprops. move => x y; split. move/(ea_relatedP fc); rewrite compf_s; move => [xs ys]. move: (iWs _ xs) (iWs _ ys)=> p1 p2. rewrite ! compfV // ! canon_proj_V // => p3;split => //. by apply/(related_equiv_P er). move => [pa pb pc]. apply /(ea_relatedP fc); aw; split => //; rewrite ! compfV // ! canon_proj_V //. + by apply: class_eq1;fprops. + Wtac. + Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)