proposition: Lemma pam_axiom f g: prod_assoc_axioms f g -> lf_axiom(fun z => (Lg (domain g) (fun l => Vf (pr_j f (Vg g l)) z))) (productb f) (productf (domain g) (fun l => (restriction_product f (Vg g l)))).
proof: Proof. move=> [fg md u] t td; apply/setXb_P; aw; split;fprops. move=> i id; rewrite !LgV //. have -> : (restriction_product f (Vg g i) = target (pr_j f (Vg g i))). by rewrite /pr_j; aw. Wtac; last by rewrite/pr_j lf_source. apply: prj_f=> // z; rewrite -u=> tu; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)