proposition: Lemma induced_rel_iirel_axioms: iirel_axioms (canonical_injection a (substrate r)) r.
proof: Proof. by move: ira=> [er ar]; split; fprops;rewrite/canonical_injection; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)