proposition: Lemma spfa_axiom f: inc f fBCA -> lf_axiom (fun x => second_partial_fun f x)B fCA.
proof: Proof. move=> pfa x xr; apply /functionsP;rewrite /second_partial_fun; hnf;aw. split => //; by apply: spf_f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)