proposition: Lemma c3f_axiom u v: function u -> function v -> lf_axiom (fun f => (v \co f) \co u) (functions (target u) (source v)) (functions (source u) (target v)).
proof: Proof. move=> fu fv x => /functionsP [fx sx tx]; apply/functionsP; hnf; aw. by split=> //; fct_tac ;[fct_tac | aw]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)