proposition: Lemma spf_axiom f x: inc f fBCA -> inc x B -> lf_axiom (fun y => Vf f (J x y)) C A.
proof: Proof. by move=> /functionsP [ff sf tf] yr y xs; Wtac; rewrite sf; apply: setXp_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)