fact: Definition canonical_foq_induced_rel r a := restriction2 (fun_on_quotients (induced_relation r a) r (canonical_injection a (substrate r))) (quotient (induced_relation r a)) (Vfs (canon_proj r) a).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)