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