proposition: Lemma fpfb_axiom: lf_axiom (fun f=> first_partial_function f) fBCA (functions C fBA).
proof: Proof. move=> x xf; apply/functionsP; rewrite / first_partial_function; split; aww. by apply: fpfa_f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)