proposition: Lemma foqcs_axioms r r' f: equivalence r -> equivalence r' -> function f -> source f = substrate r -> target f = substrate r' -> (canon_proj r' \co f) \coP (section_canon_proj r).
proof: Proof. move=> er er' ff sf tf. have fc: (function (canon_proj r')) by fprops. split; first by fct_tac => //; symmetry; aw. by apply: section_canon_proj_f. by rewrite/section_canon_proj; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)