proposition: Lemma fpfa_axiom f: inc f fBCA -> lf_axiom (fun y => (first_partial_fun f y)) C fBA.
proof: Proof. move=> pfa x xr; apply /functionsP; rewrite /first_partial_fun;hnf; aw. by split => //;apply: fpf_f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)