proposition: Lemma canonical_foq_induced_rel_fb: bijection (canonical_foq_induced_rel r a).
proof: Proof. set ci:= (canonical_injection a (substrate r)). have sf: source (fun_on_quotients (induced_relation r a) r ci) = quotient (induced_relation r a). by rewrite /fun_on_quotients/section_canon_proj; aw. have ra:restriction2_axioms (fun_on_quotients (induced_relation r a) r ci) (quotient (induced_relation r a)) (Vfs (canon_proj r) a). move: (foq_induced_rel_fi) => ifoq. split; first by fct_tac. by rewrite /fun_on_quotients/section_canon_proj; aw. rewrite /fun_on_quotients; aw; move=> t ts; move: ira=> [er ar]. by apply: (sub_im_canon_proj_quotient ar ts). by rewrite foq_induced_rel_image; fprops. split; first by apply: restriction2_fi=>//; apply: foq_induced_rel_fi. apply: restriction2_fs=>//. by rewrite - foq_induced_rel_image /Imf sf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)