proposition: Lemma spfb_axiom: lf_axiom (fun f=> second_partial_function f) fBCA (functions B fCA).
proof: Proof. move=> x xf; apply/functionsP; rewrite /second_partial_function; split; aww. by apply: spfa_f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)